# HG changeset patch
# User wenzelm
# Date 1433700220 -7200
# Node ID 51d9dcd71ad794bedcf0f49e4ee5318a8559c47b
# Parent  26dcc7f19b02b0320f43bc0de7e7097eb89f5529
tuned signature;

diff -r 26dcc7f19b02 -r 51d9dcd71ad7 src/HOL/Eisbach/eisbach_rule_insts.ML
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Sun Jun 07 15:35:49 2015 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Sun Jun 07 20:03:40 2015 +0200
@@ -81,7 +81,7 @@
     val ctxt1 =
       ctxt
       |> Context_Position.not_really
-      |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
+      |> fold_map Proof_Context.read_var fixes |-> Proof_Context.add_fixes |> #2;
 
     val typs =
       map snd type_insts
@@ -144,7 +144,7 @@
   let
     val ctxt = Context.proof_of context;
     val ctxt1 = ctxt
-      |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
+      |> fold_map Proof_Context.read_var fixes |-> Proof_Context.add_fixes |> #2;
 
     val insts' = insts @ concl_inst;
 
diff -r 26dcc7f19b02 -r 51d9dcd71ad7 src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Sun Jun 07 15:35:49 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Sun Jun 07 20:03:40 2015 +0200
@@ -113,7 +113,7 @@
     | NONE =>
         let
           val fixes' = map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
-          val (fixes'', ctxt1) = Proof_Context.read_vars fixes' ctxt;
+          val (fixes'', ctxt1) = fold_map Proof_Context.read_var fixes' ctxt;
           val (fix_nms, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
 
           val ctxt3 = Proof_Context.set_mode Proof_Context.mode_schematic ctxt2;
diff -r 26dcc7f19b02 -r 51d9dcd71ad7 src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Sun Jun 07 15:35:49 2015 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Sun Jun 07 20:03:40 2015 +0200
@@ -328,7 +328,7 @@
     fn ctxt => evaluate_method_def (match fixes) text (setup_ctxt ctxt)
   end;
 
-fun gen_method_definition prep_vars name vars uses attribs methods source lthy =
+fun gen_method_definition prep_var name vars uses attribs methods source lthy =
   let
     val (uses_nms, lthy1) = lthy
       |> Proof_Context.concealed
@@ -339,7 +339,7 @@
       |> fold_map setup_local_fact uses;
 
     val ((xs, Ts), lthy2) = lthy1
-      |> prep_vars vars |-> Proof_Context.add_fixes
+      |> fold_map prep_var vars |-> Proof_Context.add_fixes
       |-> (fn xs => fold_map Proof_Context.inferred_param xs #>> pair xs);
 
     val term_args = map Free (xs ~~ Ts);
@@ -385,8 +385,8 @@
     |> add_method name ((term_args', named_thms, method_names), text')
   end;
 
-val method_definition = gen_method_definition Proof_Context.cert_vars;
-val method_definition_cmd = gen_method_definition Proof_Context.read_vars;
+val method_definition = gen_method_definition Proof_Context.cert_var;
+val method_definition_cmd = gen_method_definition Proof_Context.read_var;
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword method} "Eisbach method definition"
diff -r 26dcc7f19b02 -r 51d9dcd71ad7 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sun Jun 07 15:35:49 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sun Jun 07 20:03:40 2015 +0200
@@ -736,7 +736,7 @@
 
 fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) =
   let
-    val (_, ctxt') = yield_singleton Proof_Context.read_vars raw_var ctxt
+    val (_, ctxt') = Proof_Context.read_var raw_var ctxt
     val rhs = (Syntax.check_term ctxt' o Syntax.parse_term ctxt') rhs_raw
     val error_msg = cat_lines
        ["Lifting failed for the following term:",
@@ -759,7 +759,7 @@
 fun lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy =
   let
     val config = evaluate_params params
-    val ((binding, SOME qty, mx), lthy) = yield_singleton Proof_Context.read_vars raw_var lthy
+    val ((binding, SOME qty, mx), lthy) = Proof_Context.read_var raw_var lthy
     val var = (binding, mx)
     val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw
     val par_thms = Attrib.eval_thms lthy par_xthms
diff -r 26dcc7f19b02 -r 51d9dcd71ad7 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Sun Jun 07 15:35:49 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sun Jun 07 20:03:40 2015 +0200
@@ -58,7 +58,7 @@
   let
     val rty = fastype_of rhs
     val qty = fastype_of lhs
-    val absrep_trm = 
+    val absrep_trm =
       Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (rty, qty) $ rhs
     val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm))
     val (_, prop') = Local_Defs.cert_def lthy prop
@@ -69,13 +69,13 @@
 
     (* data storage *)
     val qconst_data = {qconst = trm, rconst = rhs, def = def_thm}
-     
+
     fun qualify defname suffix = Binding.name suffix
       |> Binding.qualify true defname
 
     val lhs_name = Binding.name_of (#1 var)
     val rsp_thm_name = qualify lhs_name "rsp"
-    
+
     val lthy'' = lthy'
       |> Local_Theory.declaration {syntax = false, pervasive = true}
         (fn phi =>
@@ -83,7 +83,7 @@
             qcinfo as {qconst = Const (c, _), ...} =>
               Quotient_Info.update_quotconsts (c, qcinfo)
           | _ => I))
-      |> (snd oo Local_Theory.note) 
+      |> (snd oo Local_Theory.note)
         ((rsp_thm_name, @{attributes [quot_respect]}), [rsp_thm])
   in
     (qconst_data, lthy'')
@@ -92,14 +92,14 @@
 fun mk_readable_rsp_thm_eq tm lthy =
   let
     val ctm = Thm.cterm_of lthy tm
-    
-    fun norm_fun_eq ctm = 
+
+    fun norm_fun_eq ctm =
       let
         fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy
         fun erase_quants ctm' =
           case (Thm.term_of ctm') of
             Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.all_conv ctm'
-            | _ => (Conv.binder_conv (K erase_quants) lthy then_conv 
+            | _ => (Conv.binder_conv (K erase_quants) lthy then_conv
               Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
       in
         (abs_conv2 erase_quants then_conv Thm.eta_conversion) ctm
@@ -107,52 +107,55 @@
 
     fun simp_arrows_conv ctm =
       let
-        val unfold_conv = Conv.rewrs_conv 
-          [@{thm rel_fun_eq_eq_onp[THEN eq_reflection]}, @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
+        val unfold_conv = Conv.rewrs_conv
+          [@{thm rel_fun_eq_eq_onp[THEN eq_reflection]}, @{thm rel_fun_eq_rel[THEN eq_reflection]},
             @{thm rel_fun_def[THEN eq_reflection]}]
         val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
         fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
       in
         case (Thm.term_of ctm) of
-          Const (@{const_name rel_fun}, _) $ _ $ _ => 
+          Const (@{const_name rel_fun}, _) $ _ $ _ =>
             (binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm
           | _ => Conv.all_conv ctm
       end
 
-    val unfold_ret_val_invs = Conv.bottom_conv 
-      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy 
+    val unfold_ret_val_invs = Conv.bottom_conv
+      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
     val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
     val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
     val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
     val beta_conv = Thm.beta_conversion true
-    val eq_thm = 
+    val eq_thm =
       (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
   in
     Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
   end
 
 
-
-fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
+fun gen_quotient_def prep_var parse_term (raw_var, (attr, (raw_lhs, raw_rhs))) lthy =
   let
-    val (vars, ctxt) = prep_vars (the_list raw_var) lthy
-    val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE)
-    val lhs = prep_term T_opt ctxt lhs_raw
-    val rhs = prep_term NONE ctxt rhs_raw
+    val (opt_var, ctxt) =
+      (case raw_var of
+        NONE => (NONE, lthy)
+      | SOME var => prep_var var lthy |>> SOME)
+    val lhs_constraint = (case opt_var of SOME (_, SOME T, _) => T | _ => dummyT)
+
+    fun prep_term T = parse_term ctxt #> Type.constraint T #> Syntax.check_term ctxt;
+    val lhs = prep_term lhs_constraint raw_lhs
+    val rhs = prep_term dummyT raw_rhs
 
     val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
     val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
     val _ = if is_Const rhs then () else warning "The definiens is not a constant"
 
     val var =
-      (case vars of 
-        [] => (Binding.name lhs_str, NoSyn)
-      | [(binding, _, mx)] =>
+      (case opt_var of
+        NONE => (Binding.name lhs_str, NoSyn)
+      | SOME (binding, _, mx) =>
           if Variable.check_name binding = lhs_str then (binding, mx)
-          else error_msg binding lhs_str
-      | _ => raise Match)
-    
-    fun try_to_prove_refl thm = 
+          else error_msg binding lhs_str);
+
+    fun try_to_prove_refl thm =
       let
         val lhs_eq =
           thm
@@ -167,7 +170,7 @@
           | SOME _ => (case body_type (fastype_of lhs) of
             Type (typ_name, _) =>
               try (fn () =>
-                #equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name)) 
+                #equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name))
                   RS @{thm Equiv_Relations.equivp_reflp} RS thm) ()
             | _ => NONE
             )
@@ -179,32 +182,25 @@
     val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy
     val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
     val (readable_rsp_tm, _) = Logic.dest_implies (Thm.prop_of readable_rsp_thm_eq)
-  
-    fun after_qed thm_list lthy = 
+
+    fun after_qed thm_list lthy =
       let
         val internal_rsp_thm =
           case thm_list of
             [] => the maybe_proven_rsp_thm
-          | [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm 
+          | [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm
             (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt [thm] 1)
       in
         snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy)
       end
-
   in
     case maybe_proven_rsp_thm of
       SOME _ => Proof.theorem NONE after_qed [] lthy
       | NONE =>  Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy
   end
 
-fun check_term' cnstr ctxt =
-  Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I)
-
-fun read_term' cnstr ctxt =
-  check_term' cnstr ctxt o Syntax.parse_term ctxt
-
-val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term'
-val quotient_def_cmd = gen_quotient_def Proof_Context.read_vars read_term'
+val quotient_def = gen_quotient_def Proof_Context.cert_var (K I)
+val quotient_def_cmd = gen_quotient_def Proof_Context.read_var Syntax.parse_term
 
 
 (* parser and command *)
diff -r 26dcc7f19b02 -r 51d9dcd71ad7 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sun Jun 07 15:35:49 2015 +0200
+++ b/src/Pure/Isar/bundle.ML	Sun Jun 07 20:03:40 2015 +0200
@@ -57,9 +57,9 @@
 
 local
 
-fun gen_bundle prep_fact prep_att prep_vars (binding, raw_bundle) fixes lthy =
+fun gen_bundle prep_fact prep_att prep_var (binding, raw_bundle) fixes lthy =
   let
-    val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes;
+    val (_, ctxt') = lthy |> fold_map prep_var fixes |-> Proof_Context.add_fixes;
     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_vars;
-val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.read_vars;
+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;
 
 end;
 
diff -r 26dcc7f19b02 -r 51d9dcd71ad7 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Jun 07 15:35:49 2015 +0200
+++ b/src/Pure/Isar/expression.ML	Sun Jun 07 20:03:40 2015 +0200
@@ -291,11 +291,11 @@
 
 (** Prepare locale elements **)
 
-fun declare_elem prep_vars (Fixes fixes) ctxt =
-      let val (vars, _) = prep_vars fixes ctxt
+fun declare_elem prep_var (Fixes fixes) ctxt =
+      let val (vars, _) = fold_map prep_var fixes ctxt
       in ctxt |> Proof_Context.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 prep_var (Constrains csts) ctxt =
+      ctxt |> fold_map (fn (x, T) => prep_var (Binding.name x, SOME T, NoSyn)) csts |> snd
   | declare_elem _ (Assumes _) ctxt = ctxt
   | declare_elem _ (Defines _) ctxt = ctxt
   | declare_elem _ (Notes _) ctxt = ctxt;
@@ -358,7 +358,7 @@
 local
 
 fun prep_full_context_statement
-    parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
+    parse_typ parse_prop prep_var_elem prep_inst prep_var_inst prep_expr
     {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_concl ctxt1 =
   let
     val thy = Proof_Context.theory_of ctxt1;
@@ -384,7 +384,7 @@
       let
         val ctxt' = ctxt
           |> Context_Position.set_visible false
-          |> declare_elem prep_vars_elem raw_elem
+          |> declare_elem prep_var_elem raw_elem
           |> Context_Position.restore_visible ctxt;
         val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem;
       in (elems', ctxt') end;
@@ -394,7 +394,7 @@
         val concl = parse_concl parse_prop ctxt raw_concl;
       in check_autofix insts elems concl ctxt end;
 
-    val fors = prep_vars_inst fixed ctxt1 |> fst;
+    val fors = fold_map prep_var_inst fixed ctxt1 |> fst;
     val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd;
     val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
 
@@ -426,16 +426,16 @@
 in
 
 fun cert_full_context_statement x =
-  prep_full_context_statement (K I) (K I) Proof_Context.cert_vars
-  make_inst Proof_Context.cert_vars (K I) x;
+  prep_full_context_statement (K I) (K I) Proof_Context.cert_var
+  make_inst Proof_Context.cert_var (K I) x;
 
 fun cert_read_full_context_statement x =
-  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
-  make_inst Proof_Context.cert_vars (K I) x;
+  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_var
+  make_inst Proof_Context.cert_var (K I) x;
 
 fun read_full_context_statement x =
-  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
-  parse_inst Proof_Context.read_vars check_expr x;
+  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_var
+  parse_inst Proof_Context.read_var check_expr x;
 
 end;
 
diff -r 26dcc7f19b02 -r 51d9dcd71ad7 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Jun 07 15:35:49 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun Jun 07 20:03:40 2015 +0200
@@ -105,7 +105,7 @@
 
 local
 
-fun gen_obtain prep_att prep_vars prep_propp
+fun gen_obtain prep_att prep_var prep_propp
     name raw_vars raw_asms int state =
   let
     val _ = Proof.assert_forward_or_chain state;
@@ -113,7 +113,7 @@
     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
     (*obtain vars*)
-    val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
+    val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt;
     val (xs', fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
     val xs = map (Variable.check_name o #1) vars;
 
@@ -163,8 +163,8 @@
 
 in
 
-val obtain = gen_obtain (K I) Proof_Context.cert_vars Proof_Context.cert_propp;
-val obtain_cmd = gen_obtain Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.read_propp;
+val obtain = gen_obtain (K I) Proof_Context.cert_var Proof_Context.cert_propp;
+val obtain_cmd = gen_obtain Attrib.attribute_cmd Proof_Context.read_var Proof_Context.read_propp;
 
 end;
 
@@ -260,14 +260,16 @@
   let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars))
   in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end;
 
-fun gen_guess prep_vars raw_vars int state =
+fun gen_guess prep_var raw_vars int state =
   let
     val _ = Proof.assert_forward_or_chain state;
     val ctxt = Proof.context_of state;
     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
     val (thesis_var, thesis) = #1 (bind_judgment ctxt Auto_Bind.thesisN);
-    val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> fst |> polymorphic ctxt;
+    val vars = ctxt
+      |> fold_map prep_var raw_vars |-> fold_map inferred_type
+      |> fst |> polymorphic ctxt;
 
     fun guess_context raw_rule state' =
       let
@@ -314,8 +316,8 @@
 
 in
 
-val guess = gen_guess Proof_Context.cert_vars;
-val guess_cmd = gen_guess Proof_Context.read_vars;
+val guess = gen_guess Proof_Context.cert_var;
+val guess_cmd = gen_guess Proof_Context.read_var;
 
 end;
 
diff -r 26dcc7f19b02 -r 51d9dcd71ad7 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Jun 07 15:35:49 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Sun Jun 07 20:03:40 2015 +0200
@@ -591,15 +591,15 @@
 
 local
 
-fun gen_fix prep_vars args =
+fun gen_fix prep_var args =
   assert_forward
-  #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (prep_vars args ctxt)) ctxt))
+  #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (fold_map prep_var args ctxt)) ctxt))
   #> reset_facts;
 
 in
 
-val fix = gen_fix Proof_Context.cert_vars;
-val fix_cmd = gen_fix Proof_Context.read_vars;
+val fix = gen_fix Proof_Context.cert_var;
+val fix_cmd = gen_fix Proof_Context.read_var;
 
 end;
 
@@ -630,14 +630,14 @@
 
 local
 
-fun gen_def prep_att prep_vars prep_binds args state =
+fun gen_def prep_att prep_var prep_binds args state =
   let
     val _ = assert_forward state;
     val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
     val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts;
   in
     state
-    |> map_context_result (prep_vars (map (fn (x, mx) => (x, NONE, mx)) raw_vars))
+    |> map_context_result (fold_map (fn (x, mx) => prep_var (x, NONE, mx)) raw_vars)
     |>> map (fn (x, _, mx) => (x, mx))
     |-> (fn vars =>
       map_context_result (prep_binds false (map swap raw_rhss))
@@ -651,8 +651,8 @@
 
 in
 
-val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind;
-val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.match_bind_cmd;
+val def = gen_def (K I) Proof_Context.cert_var Proof_Context.match_bind;
+val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_var Proof_Context.match_bind_cmd;
 
 end;
 
diff -r 26dcc7f19b02 -r 51d9dcd71ad7 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Jun 07 15:35:49 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Jun 07 20:03:40 2015 +0200
@@ -136,10 +136,10 @@
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
-  val read_vars: (binding * string option * mixfix) list -> Proof.context ->
-    (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 read_var: binding * string option * mixfix -> Proof.context ->
+    (binding * typ option * mixfix) * Proof.context
+  val cert_var: binding * typ option * mixfix -> Proof.context ->
+    (binding * typ option * mixfix) * Proof.context
   val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
     string list * Proof.context
   val add_assms: Assumption.export ->
@@ -1063,21 +1063,20 @@
 
 local
 
-fun prep_vars prep_typ internal =
-  fold_map (fn (b, raw_T, mx) => fn ctxt =>
-    let
-      val x = check_var internal b;
-      fun cond_tvars T =
-        if internal then T
-        else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
-      val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
-      val (_, ctxt') = ctxt |> declare_var (x, opt_T, mx);
-    in ((b, opt_T, mx), ctxt') end);
+fun prep_var prep_typ internal (b, raw_T, mx) ctxt =
+  let
+    val x = check_var internal b;
+    fun cond_tvars T =
+      if internal then T
+      else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
+    val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
+    val (_, ctxt') = ctxt |> declare_var (x, opt_T, mx);
+  in ((b, opt_T, mx), ctxt') end;
 
 in
 
-val read_vars = prep_vars Syntax.read_typ false;
-val cert_vars = prep_vars (K I) true;
+val read_var = prep_var Syntax.read_typ false;
+val cert_var = prep_var (K I) true;
 
 end;
 
@@ -1168,7 +1167,7 @@
 (* fixes *)
 
 fun add_fixes raw_vars ctxt =
-  let val vars = #1 (cert_vars raw_vars ctxt) in
+  let val (vars, _) = fold_map cert_var raw_vars ctxt in
     ctxt
     |> Variable.add_fixes_binding (map #1 vars)
     |-> (fn xs =>
diff -r 26dcc7f19b02 -r 51d9dcd71ad7 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Jun 07 15:35:49 2015 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Jun 07 20:03:40 2015 +0200
@@ -87,7 +87,7 @@
 
 fun read_props raw_props raw_fixes ctxt =
   let
-    val ctxt1 = ctxt |> Proof_Context.read_vars raw_fixes |-> Proof_Context.add_fixes |> #2;
+    val ctxt1 = ctxt |> fold_map Proof_Context.read_var raw_fixes |-> Proof_Context.add_fixes |> #2;
     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;
@@ -130,9 +130,9 @@
       in fold_rev close bounds A end;
   in map close_form As end;
 
-fun prepare prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt =
+fun prepare prep_var parse_prop prep_att do_close raw_vars raw_specss ctxt =
   let
-    val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
+    val (vars, vars_ctxt) = ctxt |> fold_map prep_var raw_vars;
     val (xs, params_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
 
     val Asss =
@@ -159,23 +159,23 @@
 fun single_spec (a, prop) = [(a, [prop])];
 fun the_spec (a, [prop]) = (a, prop);
 
-fun prep_spec prep_vars parse_prop prep_att do_close vars specs =
-  prepare prep_vars parse_prop prep_att do_close
+fun prep_spec prep_var parse_prop prep_att do_close vars specs =
+  prepare prep_var parse_prop prep_att do_close
     vars (map single_spec specs) #>> apsnd (map the_spec);
 
 in
 
-fun check_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) true x;
-fun read_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.check_src true x;
+fun check_spec x = prep_spec Proof_Context.cert_var (K I) (K I) true x;
+fun read_spec x = prep_spec Proof_Context.read_var Syntax.parse_prop Attrib.check_src true x;
 
-fun check_free_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) false x;
-fun read_free_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.check_src false x;
+fun check_free_spec x = prep_spec Proof_Context.cert_var (K I) (K I) false x;
+fun read_free_spec x = prep_spec Proof_Context.read_var Syntax.parse_prop Attrib.check_src false x;
 
 fun check_specification vars specs =
-  prepare Proof_Context.cert_vars (K I) (K I) true vars [specs];
+  prepare Proof_Context.cert_var (K I) (K I) true vars [specs];
 
 fun read_specification vars specs =
-  prepare Proof_Context.read_vars Syntax.parse_prop Attrib.check_src true vars [specs];
+  prepare Proof_Context.read_var Syntax.parse_prop Attrib.check_src true vars [specs];
 
 end;
 
@@ -309,13 +309,13 @@
 
 local
 
-fun gen_theorems prep_fact prep_att prep_vars
+fun gen_theorems prep_fact prep_att prep_var
     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 |> prep_vars raw_fixes |-> Proof_Context.add_fixes;
+    val (_, ctxt') = lthy |> fold_map prep_var raw_fixes |-> Proof_Context.add_fixes;
 
     val facts' = facts
       |> Attrib.partial_evaluation ctxt'
@@ -326,8 +326,8 @@
 
 in
 
-val theorems = gen_theorems (K I) (K I) Proof_Context.cert_vars;
-val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.check_src Proof_Context.read_vars;
+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;
 
 end;
 
diff -r 26dcc7f19b02 -r 51d9dcd71ad7 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Sun Jun 07 15:35:49 2015 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Sun Jun 07 20:03:40 2015 +0200
@@ -115,7 +115,7 @@
     (*eigen-context*)
     val ctxt1 = ctxt
       |> Variable.declare_thm thm
-      |> Proof_Context.read_vars raw_fixes |-> Proof_Context.add_fixes |> #2;
+      |> fold_map Proof_Context.read_var raw_fixes |-> Proof_Context.add_fixes |> #2;
 
     (*explicit type instantiations*)
     val instT1 = Term_Subst.instantiateT (map (read_type ctxt1 tvars) type_insts);