# HG changeset patch
# User wenzelm
# Date 1309976053 -7200
# Node ID b5d1873449fb0c9ec90d53ae9529383ac4d0a2a9
# Parent  6a71db864a9167213203ead797750521a0c117d2
tuned errors;
more direct Name.uu_ for dummy abstractions;

diff -r 6a71db864a91 -r b5d1873449fb src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Jul 06 13:31:12 2011 +0200
+++ b/src/HOL/Tools/record.ML	Wed Jul 06 20:14:13 2011 +0200
@@ -718,8 +718,8 @@
                     list_comb
                       (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
                   end
-              | NONE => err ("no fields defined for " ^ ext))
-          | NONE => err (name ^ " is no proper field"))
+              | NONE => err ("no fields defined for " ^ quote ext))
+          | NONE => err (quote name ^ " is no proper field"))
       | mk_ext [] = more;
   in
     mk_ext (field_types_tr t)
@@ -753,8 +753,8 @@
                       handle Fail msg => err msg;
                     val more' = mk_ext rest;
                   in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
-              | NONE => err ("no fields defined for " ^ ext))
-          | NONE => err (name ^ " is no proper field"))
+              | NONE => err ("no fields defined for " ^ quote ext))
+          | NONE => err (quote name ^ " is no proper field"))
       | mk_ext [] = more;
   in mk_ext (fields_tr t) end;
 
@@ -766,7 +766,7 @@
 
 
 fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
-      Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg)
+      Syntax.const (suffix updateN name) $ Abs (Name.uu_, dummyT, arg)
   | field_update_tr t = raise TERM ("field_update_tr", [t]);
 
 fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
@@ -1369,7 +1369,7 @@
                             @{const_name all} => all_thm
                           | @{const_name All} => All_thm RS eq_reflection
                           | @{const_name Ex} => Ex_thm RS eq_reflection
-                          | _ => error "split_simproc"))
+                          | _ => raise Fail "split_simproc"))
                   else NONE
                 end)
           else NONE
@@ -1658,7 +1658,7 @@
     val s = Free (rN, extT);
     val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
 
-    val inject_prop =
+    val inject_prop =  (* FIXME local x x' *)
       let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
         HOLogic.mk_conj (HOLogic.eq_const extT $
           mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const)
@@ -1670,7 +1670,7 @@
     val induct_prop =
       (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
 
-    val split_meta_prop =
+    val split_meta_prop =  (* FIXME local P *)
       let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
         Logic.mk_equals
          (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
@@ -1791,6 +1791,7 @@
 
 fun mk_random_eq tyco vs extN Ts =
   let
+    (* FIXME local i etc. *)
     val size = @{term "i::code_numeral"};
     fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
     val T = Type (tyco, map TFree vs);
@@ -1810,23 +1811,25 @@
 
 fun mk_full_exhaustive_eq tyco vs extN Ts =
   let
+    (* FIXME local i etc. *)
     val size = @{term "i::code_numeral"};
     fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
     val T = Type (tyco, map TFree vs);
     val test_function = Free ("f", termifyT T --> @{typ "term list option"});
     val params = Name.invent_names Name.context "x" Ts;
-    fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
-      --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
+    fun full_exhaustiveT T =
+      (termifyT T --> @{typ "Code_Evaluation.term list option"}) -->
+        @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"};
     fun mk_full_exhaustive T =
       Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
-        full_exhaustiveT T)
+        full_exhaustiveT T);
     val lhs = mk_full_exhaustive T $ test_function $ size;
     val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
     val rhs = fold_rev (fn (v, T) => fn cont =>
-        mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc
+        mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc;
   in
     (lhs, rhs)
-  end
+  end;
 
 fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =
   let
@@ -1838,7 +1841,7 @@
     |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
     |> snd
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
-  end
+  end;
 
 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
   let
diff -r 6a71db864a91 -r b5d1873449fb src/Pure/name.ML
--- a/src/Pure/name.ML	Wed Jul 06 13:31:12 2011 +0200
+++ b/src/Pure/name.ML	Wed Jul 06 20:14:13 2011 +0200
@@ -7,6 +7,7 @@
 signature NAME =
 sig
   val uu: string
+  val uu_: string
   val aT: string
   val bound: int -> string
   val is_bound: string -> bool
@@ -35,6 +36,7 @@
 (** common defaults **)
 
 val uu = "uu";
+val uu_ = "uu_";
 val aT = "'a";
 
 
diff -r 6a71db864a91 -r b5d1873449fb src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Jul 06 13:31:12 2011 +0200
+++ b/src/Pure/term.ML	Wed Jul 06 20:14:13 2011 +0200
@@ -762,7 +762,7 @@
 
 (*Form an abstraction over a free variable.*)
 fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
-fun absdummy (T, body) = Abs (Name.internal Name.uu, T, body);
+fun absdummy (T, body) = Abs (Name.uu_, T, body);
 
 (*Abstraction over a list of free variables*)
 fun list_abs_free ([ ] ,     t) = t