--- a/src/HOL/Tools/primrec.ML Tue Apr 26 22:22:39 2011 +0200
+++ b/src/HOL/Tools/primrec.ML Wed Apr 27 10:31:18 2011 +0200
@@ -245,8 +245,7 @@
val prefix = space_implode "_" (map (Long_Name.base_name o #1) raw_defs);
fun prove lthy defs =
let
- val frees = (fold o Term.fold_aterms) (fn Free (x, _) =>
- if Variable.is_fixed lthy x then I else insert (op =) x | _ => I) eqs [];
+ val frees = fold (Variable.add_free_names lthy) eqs [];
val rewrites = rec_rewrites' @ map (snd o snd) defs;
fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
in map (fn eq => Goal.prove lthy frees [] eq tac) eqs end;
--- a/src/Pure/Isar/expression.ML Tue Apr 26 22:22:39 2011 +0200
+++ b/src/Pure/Isar/expression.ML Wed Apr 27 10:31:18 2011 +0200
@@ -380,12 +380,10 @@
val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd;
val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
- val add_free = fold_aterms
- (fn Free (x, T) => not (Variable.is_fixed ctxt3 x) ? insert (op =) (x, T) | _ => I);
val _ =
if fixed_frees then ()
else
- (case fold (fold add_free o snd o snd) insts' [] of
+ (case fold (fold (Variable.add_frees ctxt3) o snd o snd) insts' [] of
[] => ()
| frees => error ("Illegal free variables in expression: " ^
commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
--- a/src/Pure/Isar/local_defs.ML Tue Apr 26 22:22:39 2011 +0200
+++ b/src/Pure/Isar/local_defs.ML Wed Apr 27 10:31:18 2011 +0200
@@ -238,16 +238,11 @@
|> conditional ? Logic.strip_imp_concl
|> (abs_def o #2 o cert_def ctxt);
fun prove ctxt' def =
- let
- val frees = Term.fold_aterms (fn Free (x, _) =>
- if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop [];
- in
- Goal.prove ctxt' frees [] prop (K (ALLGOALS
- (CONVERSION (meta_rewrite_conv ctxt') THEN'
- rewrite_goal_tac [def] THEN'
- resolve_tac [Drule.reflexive_thm])))
- handle ERROR msg => cat_error msg "Failed to prove definitional specification"
- end;
+ Goal.prove ctxt' (Variable.add_free_names ctxt' prop []) [] prop (K (ALLGOALS
+ (CONVERSION (meta_rewrite_conv ctxt') THEN'
+ rewrite_goal_tac [def] THEN'
+ resolve_tac [Drule.reflexive_thm])))
+ handle ERROR msg => cat_error msg "Failed to prove definitional specification";
in (((c, T), rhs), prove) end;
end;
--- a/src/Pure/Isar/specification.ML Tue Apr 26 22:22:39 2011 +0200
+++ b/src/Pure/Isar/specification.ML Wed Apr 27 10:31:18 2011 +0200
@@ -88,14 +88,11 @@
fun close_forms ctxt i xs As =
let
- fun add_free (Free (x, _)) = if Variable.is_fixed ctxt x then I else insert (op =) x
- | add_free _ = I;
-
val commons = map #1 xs;
val _ =
(case duplicates (op =) commons of [] => ()
| dups => error ("Duplicate local variables " ^ commas_quote dups));
- val frees = rev ((fold o fold_aterms) add_free As (rev commons));
+ val frees = rev (fold (Variable.add_free_names ctxt) As (rev commons));
val types = map (Type_Infer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
@@ -110,7 +107,7 @@
in if Term.is_dependent B' then Term.all dummyT $ Abs (y, U, B') else B end;
fun close_form A =
let
- val occ_frees = rev (fold_aterms add_free A []);
+ val occ_frees = rev (Variable.add_free_names ctxt A []);
val bounds = xs @ map (rpair dummyT) (subtract (op =) commons occ_frees);
in fold_rev close bounds A end;
in map close_form As end;
--- a/src/Pure/variable.ML Tue Apr 26 22:22:39 2011 +0200
+++ b/src/Pure/variable.ML Wed Apr 27 10:31:18 2011 +0200
@@ -18,7 +18,6 @@
val is_declared: Proof.context -> string -> bool
val is_fixed: Proof.context -> string -> bool
val newly_fixed: Proof.context -> Proof.context -> string -> bool
- val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
val name: binding -> string
val default_type: Proof.context -> string -> typ option
val def_type: Proof.context -> bool -> indexname -> typ option
@@ -36,6 +35,10 @@
val lookup_const: Proof.context -> string -> string option
val is_const: Proof.context -> string -> bool
val declare_const: string * string -> Proof.context -> Proof.context
+ val add_fixed_names: Proof.context -> term -> string list -> string list
+ val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
+ val add_free_names: Proof.context -> term -> string list -> string list
+ val add_frees: Proof.context -> term -> (string * typ) list -> (string * typ) list
val add_fixes: string list -> Proof.context -> string list * Proof.context
val add_fixes_direct: string list -> Proof.context -> Proof.context
val auto_fixes: term -> Proof.context -> Proof.context
@@ -153,9 +156,6 @@
fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt);
fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
-fun add_fixed ctxt = Term.fold_aterms
- (fn Free (x, T) => if is_fixed ctxt x then insert (op =) (x, T) else I | _ => I);
-
(*checked name binding*)
val name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
@@ -281,6 +281,23 @@
(** fixes **)
+(* collect variables *)
+
+fun add_free_names ctxt =
+ fold_aterms (fn Free (x, _) => not (is_fixed ctxt x) ? insert (op =) x | _ => I);
+
+fun add_frees ctxt =
+ fold_aterms (fn Free (x, T) => not (is_fixed ctxt x) ? insert (op =) (x, T) | _ => I);
+
+fun add_fixed_names ctxt =
+ fold_aterms (fn Free (x, _) => is_fixed ctxt x ? insert (op =) x | _ => I);
+
+fun add_fixed ctxt =
+ fold_aterms (fn Free (x, T) => is_fixed ctxt x ? insert (op =) (x, T) | _ => I);
+
+
+(* declarations *)
+
local
fun no_dups [] = ()
@@ -324,13 +341,8 @@
|> (snd o add_fixes xs)
|> restore_body ctxt;
-fun fix_frees t ctxt = ctxt
- |> add_fixes_direct
- (rev (fold_aterms (fn Free (x, _) =>
- if is_fixed ctxt x then I else insert (op =) x | _ => I) t []));
-
-fun auto_fixes t ctxt =
- (if is_body ctxt then ctxt else fix_frees t ctxt)
+fun auto_fixes t ctxt = ctxt
+ |> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t []))
|> declare_term t;
fun invent_types Ss ctxt =