# HG changeset patch
# User wenzelm
# Date 1303893078 -7200
# Node ID 42c7ef050bc36ef74f43195184729d27af1e591f
# Parent  54450fa0d78b880cf61765aedde13d9479915331
more uniform Variable.add_frees/add_fixed etc.;

diff -r 54450fa0d78b -r 42c7ef050bc3 src/HOL/Tools/primrec.ML
--- 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;
diff -r 54450fa0d78b -r 42c7ef050bc3 src/Pure/Isar/expression.ML
--- 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))));
diff -r 54450fa0d78b -r 42c7ef050bc3 src/Pure/Isar/local_defs.ML
--- 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;
diff -r 54450fa0d78b -r 42c7ef050bc3 src/Pure/Isar/specification.ML
--- 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;
diff -r 54450fa0d78b -r 42c7ef050bc3 src/Pure/variable.ML
--- 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 =