# HG changeset patch
# User wenzelm
# Date 1519570933 -3600
#      Sun Feb 25 16:02:13 2018 +0100
# Node ID c114051a18cc1c97978e101b308e4c180c6d1ec2
# Parent  5348bea4accdc357f1248e62ea4331c0392f7e60
test

diff -r 5348bea4accd -r c114051a18cc src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sun Feb 25 15:44:46 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sun Feb 25 16:02:13 2018 +0100
@@ -44,16 +44,24 @@
 parse_translation \<open>
   let
     fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
-    fun finite_vec_tr [t, u] =
-      (case Term_Position.strip_positions u of
-        v as Free (x, _) =>
-          if Lexicon.is_tid x then
-            vec t (Syntax.const @{syntax_const "_ofsort"} $ v $
-              Syntax.const @{class_syntax finite})
-          else vec t u
-      | _ => vec t u)
+    fun finite_vec_tr ctxt [t, u] =
+      let
+        fun warn s =
+          if Context_Position.is_visible ctxt
+          then warning ("FIXME " ^ s ^ Position.here (Position.thread_data ()))
+          else ();
+      in
+        (case Term_Position.strip_positions u of
+          v as Free (x, _) =>
+            if Lexicon.is_tid x then
+              (warn "vec1";
+              vec t (Syntax.const @{syntax_const "_ofsort"} $ v $
+                Syntax.const @{class_syntax finite}))
+            else (warn "vec2"; vec t u)
+        | _ => (warn "vec3"; vec t u))
+      end;
   in
-    [(@{syntax_const "_finite_vec"}, K finite_vec_tr)]
+    [(@{syntax_const "_finite_vec"}, finite_vec_tr)]
   end
 \<close>