# HG changeset patch
# User wenzelm
# Date 1434289993 -7200
# Node ID d1ea37df73587538efb188402024f97199a493c6
# Parent  4ba2a8bc5c362fad64c34397e61658039a3e1469
tuned signature;

diff -r 4ba2a8bc5c36 -r d1ea37df7358 src/HOL/Eisbach/eisbach_rule_insts.ML
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Sun Jun 14 14:59:39 2015 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Sun Jun 14 15:53:13 2015 +0200
@@ -81,7 +81,7 @@
     val ctxt1 =
       ctxt
       |> Context_Position.not_really
-      |> fold_map Proof_Context.read_var fixes |-> Proof_Context.add_fixes |> #2;
+      |> Proof_Context.add_fixes_cmd fixes |> #2;
 
     val typs =
       map snd type_insts
@@ -140,11 +140,10 @@
 val inst =  Args.maybe Parse_Tools.name_term;
 val concl = Args.$$$ "concl" -- Args.colon;
 
-fun close_unchecked_insts context ((insts,concl_inst), fixes) =
+fun close_unchecked_insts context ((insts, concl_inst), fixes) =
   let
     val ctxt = Context.proof_of context;
-    val ctxt1 = ctxt
-      |> fold_map Proof_Context.read_var fixes |-> Proof_Context.add_fixes |> #2;
+    val ctxt1 = ctxt |> Proof_Context.add_fixes_cmd fixes |> #2;
 
     val insts' = insts @ concl_inst;
 
diff -r 4ba2a8bc5c36 -r d1ea37df7358 src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Sun Jun 14 14:59:39 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Sun Jun 14 15:53:13 2015 +0200
@@ -112,11 +112,10 @@
     | SOME _ => error "Unexpected token value in match cartouche"
     | NONE =>
         let
-          val fixes' = map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
-          val (fixes'', ctxt1) = fold_map Proof_Context.read_var fixes' ctxt;
-          val (fix_names, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
-
-          val ctxt3 = Proof_Context.set_mode Proof_Context.mode_schematic ctxt2;
+          val (fix_names, ctxt3) = ctxt
+            |> Proof_Context.add_fixes_cmd
+              (map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes)
+            ||> Proof_Context.set_mode Proof_Context.mode_schematic;
 
           fun parse_term term =
             if prop_match match_kind
diff -r 4ba2a8bc5c36 -r d1ea37df7358 src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Sun Jun 14 14:59:39 2015 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Sun Jun 14 15:53:13 2015 +0200
@@ -328,7 +328,7 @@
     fn ctxt => evaluate_method_def (match fixes) text (setup_ctxt ctxt)
   end;
 
-fun gen_method_definition prep_var name vars uses attribs methods source lthy =
+fun gen_method_definition add_fixes name vars uses attribs methods source lthy =
   let
     val (uses_nms, lthy1) = lthy
       |> Proof_Context.concealed
@@ -339,8 +339,7 @@
       |> fold_map setup_local_fact uses;
 
     val (term_args, lthy2) = lthy1
-      |> fold_map prep_var vars |-> Proof_Context.add_fixes
-      |-> fold_map Proof_Context.inferred_param |>> map Free;
+      |> add_fixes vars |-> fold_map Proof_Context.inferred_param |>> map Free;
 
     val (named_thms, modifiers) = map (check_attrib lthy2) (attribs @ uses) |> split_list;
     val self_name :: method_names = map (Local_Theory.full_name lthy2) (name :: methods);
@@ -384,8 +383,8 @@
     |> add_method name ((term_args', named_thms, method_names), text')
   end;
 
-val method_definition = gen_method_definition Proof_Context.cert_var;
-val method_definition_cmd = gen_method_definition Proof_Context.read_var;
+val method_definition = gen_method_definition Proof_Context.add_fixes;
+val method_definition_cmd = gen_method_definition Proof_Context.add_fixes_cmd;
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword method} "Eisbach method definition"
diff -r 4ba2a8bc5c36 -r d1ea37df7358 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sun Jun 14 14:59:39 2015 +0200
+++ b/src/Pure/Isar/bundle.ML	Sun Jun 14 15:53:13 2015 +0200
@@ -57,9 +57,9 @@
 
 local
 
-fun gen_bundle prep_fact prep_att prep_var (binding, raw_bundle) fixes lthy =
+fun gen_bundle prep_fact prep_att add_fixes (binding, raw_bundle) raw_fixes lthy =
   let
-    val (_, ctxt') = lthy |> fold_map prep_var fixes |-> Proof_Context.add_fixes;
+    val (_, ctxt') = add_fixes raw_fixes lthy;
     val bundle0 = raw_bundle
       |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts));
     val bundle =
@@ -75,8 +75,8 @@
 
 in
 
-val bundle = gen_bundle (K I) (K I) Proof_Context.cert_var;
-val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.read_var;
+val bundle = gen_bundle (K I) (K I) Proof_Context.add_fixes;
+val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.add_fixes_cmd;
 
 end;
 
diff -r 4ba2a8bc5c36 -r d1ea37df7358 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Jun 14 14:59:39 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Sun Jun 14 15:53:13 2015 +0200
@@ -594,15 +594,15 @@
 
 local
 
-fun gen_fix prep_var args =
+fun gen_fix add_fixes raw_fixes =
   assert_forward
-  #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (fold_map prep_var args ctxt)) ctxt))
+  #> map_context (snd o add_fixes raw_fixes)
   #> reset_facts;
 
 in
 
-val fix = gen_fix Proof_Context.cert_var;
-val fix_cmd = gen_fix Proof_Context.read_var;
+val fix = gen_fix Proof_Context.add_fixes;
+val fix_cmd = gen_fix Proof_Context.add_fixes_cmd;
 
 end;
 
diff -r 4ba2a8bc5c36 -r d1ea37df7358 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Jun 14 14:59:39 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Jun 14 15:53:13 2015 +0200
@@ -131,6 +131,8 @@
     (binding * typ option * mixfix) * Proof.context
   val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
     string list * Proof.context
+  val add_fixes_cmd: (binding * string option * mixfix) list -> Proof.context ->
+    string list * Proof.context
   val add_assms: Assumption.export ->
     (Thm.binding * (term * term list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
@@ -1131,16 +1133,26 @@
 
 (* fixes *)
 
-fun add_fixes raw_vars ctxt =
-  let val (vars, _) = fold_map cert_var raw_vars ctxt in
-    ctxt
-    |> Variable.add_fixes_binding (map #1 vars)
-    |-> (fn xs =>
-      fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
-      #-> (map_syntax_idents o Local_Syntax.add_syntax ctxt o map (pair Local_Syntax.Fixed))
-      #> pair xs)
+local
+
+fun gen_fixes prep_var raw_vars ctxt =
+  let
+    val (vars, _) = fold_map prep_var raw_vars ctxt;
+    val (xs, ctxt') = Variable.add_fixes_binding (map #1 vars) ctxt;
+  in
+    ctxt'
+    |> fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
+    |-> (map_syntax_idents o Local_Syntax.add_syntax ctxt o map (pair Local_Syntax.Fixed))
+    |> pair xs
   end;
 
+in
+
+val add_fixes = gen_fixes cert_var;
+val add_fixes_cmd = gen_fixes read_var;
+
+end;
+
 
 
 (** assumptions **)
diff -r 4ba2a8bc5c36 -r d1ea37df7358 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Jun 14 14:59:39 2015 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Jun 14 15:53:13 2015 +0200
@@ -87,7 +87,7 @@
 
 fun read_props raw_props raw_fixes ctxt =
   let
-    val ctxt1 = ctxt |> fold_map Proof_Context.read_var raw_fixes |-> Proof_Context.add_fixes |> #2;
+    val (_, ctxt1) = ctxt |> Proof_Context.add_fixes_cmd raw_fixes;
     val props1 = map (Syntax.parse_prop ctxt1) raw_props;
     val (props2, ctxt2) = ctxt1 |> fold_map Variable.fix_dummy_patterns props1;
     val props3 = Syntax.check_props ctxt2 props2;
@@ -291,13 +291,13 @@
 
 local
 
-fun gen_theorems prep_fact prep_att prep_var
+fun gen_theorems prep_fact prep_att add_fixes
     kind raw_facts raw_fixes int lthy =
   let
     val facts = raw_facts |> map (fn ((name, atts), bs) =>
       ((name, map (prep_att lthy) atts),
         bs |> map (fn (b, more_atts) => (prep_fact lthy b, map (prep_att lthy) more_atts))));
-    val (_, ctxt') = lthy |> fold_map prep_var raw_fixes |-> Proof_Context.add_fixes;
+    val (_, ctxt') = add_fixes raw_fixes lthy;
 
     val facts' = facts
       |> Attrib.partial_evaluation ctxt'
@@ -308,8 +308,8 @@
 
 in
 
-val theorems = gen_theorems (K I) (K I) Proof_Context.cert_var;
-val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.check_src Proof_Context.read_var;
+val theorems = gen_theorems (K I) (K I) Proof_Context.add_fixes;
+val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.check_src Proof_Context.add_fixes_cmd;
 
 end;
 
diff -r 4ba2a8bc5c36 -r d1ea37df7358 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Sun Jun 14 14:59:39 2015 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Sun Jun 14 15:53:13 2015 +0200
@@ -113,9 +113,9 @@
     val vars = Thm.fold_terms Term.add_vars thm [];
 
     (*eigen-context*)
-    val ctxt1 = ctxt
+    val (_, ctxt1) = ctxt
       |> Variable.declare_thm thm
-      |> fold_map Proof_Context.read_var raw_fixes |-> Proof_Context.add_fixes |> #2;
+      |> Proof_Context.add_fixes_cmd raw_fixes;
 
     (*explicit type instantiations*)
     val instT1 = Term_Subst.instantiateT (map (read_type ctxt1 tvars) type_insts);