# HG changeset patch
# User wenzelm
# Date 1238259213 -3600
# Node ID 6976521b4263a029011a8e3e246492c001f04763
# Parent  cabf9ff3a129c7e0c57a38d4f6b3dfb737ea1af7
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;

diff -r cabf9ff3a129 -r 6976521b4263 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Mar 28 17:21:49 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Mar 28 17:53:33 2009 +0100
@@ -181,7 +181,7 @@
       | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));
     fun mk_avoids params name sets =
       let
-        val (_, ctxt') = ProofContext.add_fixes_i
+        val (_, ctxt') = ProofContext.add_fixes
           (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt;
         fun mk s =
           let
diff -r cabf9ff3a129 -r 6976521b4263 src/HOL/Tools/function_package/fundef_lib.ML
--- a/src/HOL/Tools/function_package/fundef_lib.ML	Sat Mar 28 17:21:49 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Sat Mar 28 17:53:33 2009 +0100
@@ -55,7 +55,7 @@
 fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
     let
       val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
-      val (_, ctx') = ProofContext.add_fixes_i [(Binding.name n', SOME T, NoSyn)] ctx
+      val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
 
       val (n'', body) = Term.dest_abs (n', T, b) 
       val _ = (n' = n'') orelse error "dest_all_ctx"
diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Sat Mar 28 17:21:49 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML	Sat Mar 28 17:53:33 2009 +0100
@@ -25,13 +25,13 @@
     fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
 
     val thy_ctxt = ProofContext.init thy;
-    val struct_ctxt = #2 (ProofContext.add_fixes_i structs thy_ctxt);
+    val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt);
     val ((d, mx), var_ctxt) =
       (case raw_decl of
         NONE => ((NONE, NoSyn), struct_ctxt)
       | SOME raw_var =>
           struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
-            ProofContext.add_fixes_i [(x, T, mx)] #> snd #> pair (SOME x, mx)));
+            ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx)));
 
     val prop = prep_prop var_ctxt raw_prop;
     val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Mar 28 17:21:49 2009 +0100
+++ b/src/Pure/Isar/element.ML	Sat Mar 28 17:53:33 2009 +0100
@@ -486,7 +486,7 @@
 local
 
 fun activate_elem (Fixes fixes) ctxt =
-      ctxt |> ProofContext.add_fixes_i fixes |> snd
+      ctxt |> ProofContext.add_fixes fixes |> snd
   | activate_elem (Constrains _) ctxt =
       ctxt
   | activate_elem (Assumes asms) ctxt =
diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sat Mar 28 17:21:49 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Mar 28 17:53:33 2009 +0100
@@ -271,7 +271,7 @@
 
 fun declare_elem prep_vars (Fixes fixes) ctxt =
       let val (vars, _) = prep_vars fixes ctxt
-      in ctxt |> ProofContext.add_fixes_i vars |> snd end
+      in ctxt |> ProofContext.add_fixes vars |> snd end
   | declare_elem prep_vars (Constrains csts) ctxt =
       ctxt |> prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) |> snd
   | declare_elem _ (Assumes _) ctxt = ctxt
@@ -368,7 +368,7 @@
       in check_autofix insts elems concl ctxt end;
 
     val fors = prep_vars_inst fixed ctxt1 |> fst;
-    val ctxt2 = ctxt1 |> ProofContext.add_fixes_i fors |> snd;
+    val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
     val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
     val ctxt4 = init_body ctxt3;
     val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
@@ -426,7 +426,7 @@
 (* Locale declaration: import + elements *)
 
 fun fix_params params =
-  ProofContext.add_fixes_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
+  ProofContext.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
 
 local
 
diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sat Mar 28 17:21:49 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Sat Mar 28 17:53:33 2009 +0100
@@ -96,7 +96,7 @@
     val lhss = map (fst o Logic.dest_equals) eqs;
   in
     ctxt
-    |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
+    |> ProofContext.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
     |> fold Variable.declare_term eqs
     |> ProofContext.add_assms_i def_export
       (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
@@ -115,7 +115,7 @@
     val T = Term.fastype_of rhs;
     val ([x'], ctxt') = ctxt
       |> Variable.declare_term rhs
-      |> ProofContext.add_fixes_i [(x, SOME T, mx)];
+      |> ProofContext.add_fixes [(x, SOME T, mx)];
     val lhs = Free (x', T);
     val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs));
     fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);
diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Mar 28 17:21:49 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Mar 28 17:53:33 2009 +0100
@@ -306,7 +306,7 @@
   in PureThy.note_thmss kind facts' thy |> snd end
 
 fun init_local_elem (Fixes fixes) ctxt = ctxt |>
-      ProofContext.add_fixes_i fixes |> snd
+      ProofContext.add_fixes fixes |> snd
   | init_local_elem (Assumes assms) ctxt =
       let
         val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms
diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Mar 28 17:21:49 2009 +0100
+++ b/src/Pure/Isar/obtain.ML	Sat Mar 28 17:53:33 2009 +0100
@@ -118,7 +118,7 @@
 
     (*obtain vars*)
     val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
-    val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
+    val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
     val xs = map (Name.of_binding o #1) vars;
 
     (*obtain asms*)
diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Mar 28 17:21:49 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Mar 28 17:53:33 2009 +0100
@@ -531,15 +531,15 @@
 
 local
 
-fun gen_fix add_fixes args =
+fun gen_fix prep_vars args =
   assert_forward
-  #> map_context (snd o add_fixes args)
+  #> map_context (fn ctxt => snd (ProofContext.add_fixes (prep_vars ctxt args) ctxt))
   #> put_facts NONE;
 
 in
 
-val fix = gen_fix ProofContext.add_fixes;
-val fix_i = gen_fix ProofContext.add_fixes_i;
+val fix = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
+val fix_i = gen_fix (K I);
 
 end;
 
diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Mar 28 17:21:49 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 28 17:53:33 2009 +0100
@@ -108,10 +108,8 @@
     (binding * typ option * mixfix) list * Proof.context
   val cert_vars: (binding * typ option * mixfix) list -> Proof.context ->
     (binding * typ option * mixfix) list * Proof.context
-  val add_fixes: (binding * string option * mixfix) list ->
-    Proof.context -> string list * Proof.context
-  val add_fixes_i: (binding * typ option * mixfix) list ->
-    Proof.context -> string list * Proof.context
+  val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
+    string list * Proof.context
   val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
   val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
   val add_assms: Assumption.export ->
@@ -1105,9 +1103,11 @@
     error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x)
   else (true, (x, T, mx));
 
-fun gen_fixes prep raw_vars ctxt =
+in
+
+fun add_fixes raw_vars ctxt =
   let
-    val (vars, _) = prep raw_vars ctxt;
+    val (vars, _) = cert_vars raw_vars ctxt;
     val (xs', ctxt') = Variable.add_fixes (map (Name.of_binding o #1) vars) ctxt;
     val ctxt'' =
       ctxt'
@@ -1117,11 +1117,6 @@
       ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
   in (xs', ctxt'') end;
 
-in
-
-val add_fixes = gen_fixes read_vars;
-val add_fixes_i = gen_fixes cert_vars;
-
 end;
 
 
@@ -1132,7 +1127,7 @@
 
 fun bind_fixes xs ctxt =
   let
-    val (_, ctxt') = ctxt |> add_fixes_i (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
+    val (_, ctxt') = ctxt |> add_fixes (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
     fun bind (t as Free (x, T)) =
           if member (op =) xs x then
             (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t)
diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Sat Mar 28 17:21:49 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Sat Mar 28 17:53:33 2009 +0100
@@ -283,7 +283,7 @@
         val (param_names, ctxt') = ctxt
           |> Variable.declare_thm thm
           |> Thm.fold_terms Variable.declare_constraints st
-          |> ProofContext.add_fixes_i (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
+          |> ProofContext.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
 
         (* Process type insts: Tinsts_env *)
         fun absent xi = error
diff -r cabf9ff3a129 -r 6976521b4263 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Mar 28 17:21:49 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Mar 28 17:53:33 2009 +0100
@@ -108,7 +108,7 @@
     val thy = ProofContext.theory_of ctxt;
 
     val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
-    val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
+    val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
 
     val Asss = (map o map) (map (parse_prop params_ctxt) o snd) raw_specss;
     val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
@@ -312,7 +312,7 @@
               |> fold_map ProofContext.inferred_param xs;
             val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
           in
-            ctxt' |> (snd o ProofContext.add_fixes_i (map (fn b => (b, NONE, NoSyn)) bs));
+            ctxt' |> (snd o ProofContext.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
             ctxt' |> Variable.auto_fixes asm
             |> ProofContext.add_assms_i Assumption.assume_export
               [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
@@ -325,7 +325,7 @@
         val stmt = [((Binding.empty, atts), [(thesis, [])])];
 
         val (facts, goal_ctxt) = elems_ctxt
-          |> (snd o ProofContext.add_fixes_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
+          |> (snd o ProofContext.add_fixes [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
           |> fold_map assume_case (obtains ~~ propp)
           |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
                 [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);