# HG changeset patch
# User wenzelm
# Date 1433860937 -7200
# Node ID 53ef7b78e78a16b9407d65b12751fce8749fa8a4
# Parent  12cc54fac9b028382252607e8a0b296f02efd4bc
tuned signature;

diff -r 12cc54fac9b0 -r 53ef7b78e78a src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Tue Jun 09 16:07:11 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Tue Jun 09 16:42:17 2015 +0200
@@ -114,7 +114,7 @@
         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_nms, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
+          val (fix_names, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
 
           val ctxt3 = Proof_Context.set_mode Proof_Context.mode_schematic ctxt2;
 
@@ -147,15 +147,14 @@
             map2 (fn nm => fn (_, pos) =>
                 member (op =) pat_fixes nm orelse
                 error ("For-fixed variable must be bound in some pattern" ^ Position.here pos))
-              fix_nms fixes;
+              fix_names fixes;
 
           val _ = map (Term.map_types Type.no_tvars) pats;
 
           val ctxt4 = fold Variable.declare_term pats ctxt3;
 
-          val (Ts, ctxt5) = ctxt4 |> fold_map Proof_Context.inferred_param fix_nms;
-
-          val real_fixes = map Free (fix_nms ~~ Ts);
+          val (real_fixes, ctxt5) = ctxt4
+            |> fold_map Proof_Context.inferred_param fix_names |>> map Free;
 
           fun reject_extra_free (Free (x, _)) () =
                 if Variable.is_fixed ctxt5 x then ()
diff -r 12cc54fac9b0 -r 53ef7b78e78a src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Tue Jun 09 16:07:11 2015 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Tue Jun 09 16:42:17 2015 +0200
@@ -338,11 +338,10 @@
       |> fold setup_local_method methods
       |> fold_map setup_local_fact uses;
 
-    val ((xs, Ts), lthy2) = lthy1
+    val (term_args, lthy2) = lthy1
       |> fold_map prep_var vars |-> Proof_Context.add_fixes
-      |-> (fn xs => fold_map Proof_Context.inferred_param xs #>> pair xs);
+      |-> fold_map Proof_Context.inferred_param |>> map Free;
 
-    val term_args = map Free (xs ~~ Ts);
     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);
 
diff -r 12cc54fac9b0 -r 53ef7b78e78a src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Jun 09 16:07:11 2015 +0200
+++ b/src/Pure/Isar/expression.ML	Tue Jun 09 16:42:17 2015 +0200
@@ -410,11 +410,12 @@
     val (elems, ctxt5) = fold_map prep_elem raw_elems ctxt4;
     val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
 
-    (* Retrieve parameter types *)
+
+    (* parameters from expression and elements *)
+
     val xs = maps (fn Fixes fixes => map (Variable.check_name o #1) fixes | _ => [])
       (Fixes fors :: elems');
-    val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
-    val parms = xs ~~ Ts;  (* params from expression and elements *)
+    val (parms, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
 
     val fors' = finish_fixes parms fors;
     val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
diff -r 12cc54fac9b0 -r 53ef7b78e78a src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Jun 09 16:07:11 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Jun 09 16:42:17 2015 +0200
@@ -127,8 +127,8 @@
       map (map (rpair [])) asm_propss;
 
     (*obtain params*)
-    val (Ts, params_ctxt) = fold_map Proof_Context.inferred_param xs' (declare_asms fix_ctxt);
-    val params = map Free (xs' ~~ Ts);
+    val (params, params_ctxt) =
+      declare_asms fix_ctxt |> fold_map Proof_Context.inferred_param xs' |>> map Free;
     val cparams = map (Thm.cterm_of params_ctxt) params;
     val binds' = map (apsnd (fold_rev Term.dependent_lambda_name (xs ~~ params))) binds;
 
@@ -259,7 +259,7 @@
 fun inferred_type (binding, _, mx) ctxt =
   let
     val x = Variable.check_name binding;
-    val (T, ctxt') = Proof_Context.inferred_param x ctxt
+    val ((_, T), ctxt') = Proof_Context.inferred_param x ctxt
   in ((x, T, mx), ctxt') end;
 
 fun polymorphic ctxt vars =
diff -r 12cc54fac9b0 -r 53ef7b78e78a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Jun 09 16:07:11 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jun 09 16:42:17 2015 +0200
@@ -991,13 +991,13 @@
           |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
 
         val (propss, binds) = prep_propp fix_ctxt propp;
-        val (Ts, params_ctxt) = fix_ctxt
+        val (ps, params_ctxt) = fix_ctxt
           |> (fold o fold) Variable.declare_term propss
           |> Proof_Context.bind_terms binds
           |> fold_map Proof_Context.inferred_param xs';
 
         val xs = map (Variable.check_name o #1) vars;
-        val params = xs ~~ map Free (xs' ~~ Ts);
+        val params = xs ~~ map Free ps;
 
         val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
       in ((propss, params, binds), params_ctxt) end;
diff -r 12cc54fac9b0 -r 53ef7b78e78a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jun 09 16:07:11 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jun 09 16:42:17 2015 +0200
@@ -74,7 +74,7 @@
   val cert_typ_syntax: Proof.context -> typ -> typ
   val cert_typ_abbrev: Proof.context -> typ -> typ
   val infer_type: Proof.context -> string * typ -> typ
-  val inferred_param: string -> Proof.context -> typ * Proof.context
+  val inferred_param: string -> Proof.context -> (string * typ) * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
   val check_type_name: {proper: bool, strict: bool} -> Proof.context ->
     xstring * Position.T -> typ * Position.report list
@@ -458,14 +458,11 @@
   Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x));
 
 fun inferred_param x ctxt =
-  let val T = infer_type ctxt (x, dummyT)
-  in (T, ctxt |> Variable.declare_term (Free (x, T))) end;
+  let val p = (x, infer_type ctxt (x, dummyT))
+  in (p, ctxt |> Variable.declare_term (Free p)) end;
 
 fun inferred_fixes ctxt =
-  let
-    val xs = map #2 (Variable.dest_fixes ctxt);
-    val (Ts, ctxt') = fold_map inferred_param xs ctxt;
-  in (xs ~~ Ts, ctxt') end;
+  fold_map inferred_param (map #2 (Variable.dest_fixes ctxt)) ctxt;
 
 
 (* type names *)
diff -r 12cc54fac9b0 -r 53ef7b78e78a src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Jun 09 16:07:11 2015 +0200
+++ b/src/Pure/Isar/specification.ML	Tue Jun 09 16:42:17 2015 +0200
@@ -150,8 +150,8 @@
       |> flat |> burrow (Syntax.check_props params_ctxt);
     val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
 
-    val Ts = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
-    val params = map2 (fn (b, _, mx) => fn T => ((b, T), mx)) vars Ts;
+    val ps = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
+    val params = map2 (fn (b, _, mx) => fn (_, T) => ((b, T), mx)) vars ps;
     val name_atts = map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (flat raw_specss);
   in ((params, name_atts ~~ specs), specs_ctxt) end;
 
@@ -363,10 +363,10 @@
             val bs = map fst vars;
             val xs = map Variable.check_name bs;
             val props = map fst asms;
-            val (Ts, _) = ctxt'
+            val (params, _) = ctxt'
               |> fold Variable.declare_term props
-              |> fold_map Proof_Context.inferred_param xs;
-            val params = map Free (xs ~~ Ts);
+              |> fold_map Proof_Context.inferred_param xs
+              |>> map Free;
             val asm = fold_rev Logic.all params (Logic.list_implies (props, thesis));
             val _ = ctxt' |> Proof_Context.add_fixes (map (fn b => (b, NONE, NoSyn)) bs);
           in