1.1 --- a/src/HOL/Tools/record.ML Wed Jul 06 13:31:12 2011 +0200
1.2 +++ b/src/HOL/Tools/record.ML Wed Jul 06 20:14:13 2011 +0200
1.3 @@ -718,8 +718,8 @@
1.4 list_comb
1.5 (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
1.6 end
1.7 - | NONE => err ("no fields defined for " ^ ext))
1.8 - | NONE => err (name ^ " is no proper field"))
1.9 + | NONE => err ("no fields defined for " ^ quote ext))
1.10 + | NONE => err (quote name ^ " is no proper field"))
1.11 | mk_ext [] = more;
1.12 in
1.13 mk_ext (field_types_tr t)
1.14 @@ -753,8 +753,8 @@
1.15 handle Fail msg => err msg;
1.16 val more' = mk_ext rest;
1.17 in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
1.18 - | NONE => err ("no fields defined for " ^ ext))
1.19 - | NONE => err (name ^ " is no proper field"))
1.20 + | NONE => err ("no fields defined for " ^ quote ext))
1.21 + | NONE => err (quote name ^ " is no proper field"))
1.22 | mk_ext [] = more;
1.23 in mk_ext (fields_tr t) end;
1.24
1.25 @@ -766,7 +766,7 @@
1.26
1.27
1.28 fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
1.29 - Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg)
1.30 + Syntax.const (suffix updateN name) $ Abs (Name.uu_, dummyT, arg)
1.31 | field_update_tr t = raise TERM ("field_update_tr", [t]);
1.32
1.33 fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
1.34 @@ -1369,7 +1369,7 @@
1.35 @{const_name all} => all_thm
1.36 | @{const_name All} => All_thm RS eq_reflection
1.37 | @{const_name Ex} => Ex_thm RS eq_reflection
1.38 - | _ => error "split_simproc"))
1.39 + | _ => raise Fail "split_simproc"))
1.40 else NONE
1.41 end)
1.42 else NONE
1.43 @@ -1658,7 +1658,7 @@
1.44 val s = Free (rN, extT);
1.45 val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
1.46
1.47 - val inject_prop =
1.48 + val inject_prop = (* FIXME local x x' *)
1.49 let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
1.50 HOLogic.mk_conj (HOLogic.eq_const extT $
1.51 mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const)
1.52 @@ -1670,7 +1670,7 @@
1.53 val induct_prop =
1.54 (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
1.55
1.56 - val split_meta_prop =
1.57 + val split_meta_prop = (* FIXME local P *)
1.58 let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
1.59 Logic.mk_equals
1.60 (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
1.61 @@ -1791,6 +1791,7 @@
1.62
1.63 fun mk_random_eq tyco vs extN Ts =
1.64 let
1.65 + (* FIXME local i etc. *)
1.66 val size = @{term "i::code_numeral"};
1.67 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
1.68 val T = Type (tyco, map TFree vs);
1.69 @@ -1810,23 +1811,25 @@
1.70
1.71 fun mk_full_exhaustive_eq tyco vs extN Ts =
1.72 let
1.73 + (* FIXME local i etc. *)
1.74 val size = @{term "i::code_numeral"};
1.75 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
1.76 val T = Type (tyco, map TFree vs);
1.77 val test_function = Free ("f", termifyT T --> @{typ "term list option"});
1.78 val params = Name.invent_names Name.context "x" Ts;
1.79 - fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
1.80 - --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
1.81 + fun full_exhaustiveT T =
1.82 + (termifyT T --> @{typ "Code_Evaluation.term list option"}) -->
1.83 + @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"};
1.84 fun mk_full_exhaustive T =
1.85 Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
1.86 - full_exhaustiveT T)
1.87 + full_exhaustiveT T);
1.88 val lhs = mk_full_exhaustive T $ test_function $ size;
1.89 val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
1.90 val rhs = fold_rev (fn (v, T) => fn cont =>
1.91 - mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc
1.92 + mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc;
1.93 in
1.94 (lhs, rhs)
1.95 - end
1.96 + end;
1.97
1.98 fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =
1.99 let
1.100 @@ -1838,7 +1841,7 @@
1.101 |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
1.102 |> snd
1.103 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
1.104 - end
1.105 + end;
1.106
1.107 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
1.108 let
2.1 --- a/src/Pure/name.ML Wed Jul 06 13:31:12 2011 +0200
2.2 +++ b/src/Pure/name.ML Wed Jul 06 20:14:13 2011 +0200
2.3 @@ -7,6 +7,7 @@
2.4 signature NAME =
2.5 sig
2.6 val uu: string
2.7 + val uu_: string
2.8 val aT: string
2.9 val bound: int -> string
2.10 val is_bound: string -> bool
2.11 @@ -35,6 +36,7 @@
2.12 (** common defaults **)
2.13
2.14 val uu = "uu";
2.15 +val uu_ = "uu_";
2.16 val aT = "'a";
2.17
2.18
3.1 --- a/src/Pure/term.ML Wed Jul 06 13:31:12 2011 +0200
3.2 +++ b/src/Pure/term.ML Wed Jul 06 20:14:13 2011 +0200
3.3 @@ -762,7 +762,7 @@
3.4
3.5 (*Form an abstraction over a free variable.*)
3.6 fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
3.7 -fun absdummy (T, body) = Abs (Name.internal Name.uu, T, body);
3.8 +fun absdummy (T, body) = Abs (Name.uu_, T, body);
3.9
3.10 (*Abstraction over a list of free variables*)
3.11 fun list_abs_free ([ ] , t) = t