tuned signature;

--- a/src/Pure/Isar/proof.ML	Sun Jun 07 23:37:32 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Jun 08 14:45:31 2015 +0200
@@ -998,16 +998,21 @@
 
 (* global goals *)
 
-fun prepp_auto_fixes prepp args =
-  prepp args #>
-  (fn ((propss, a), ctxt) => ((propss, a), (fold o fold) Variable.auto_fixes propss ctxt));
+fun global_goal prepp before_qed after_qed propp =
+  let
+    fun prepp' args ctxt1 =
+      let
+        val ((propss, binds), ctxt2) = ctxt1
+          |> Proof_Context.set_mode Proof_Context.mode_schematic
+          |> prepp args;
+        val ctxt3 = ctxt2
+          |> (fold o fold) Variable.auto_fixes propss
+          |> Proof_Context.restore_mode ctxt1;
+      in ((propss, binds), ctxt3) end;
+  in init #> generic_goal prepp' "" before_qed (K I, after_qed) propp end;
 
-fun global_goal prepp before_qed after_qed propp =
-  init #>
-  generic_goal (prepp_auto_fixes prepp) "" before_qed (K I, after_qed) propp;
-
-val theorem = global_goal Proof_Context.bind_propp_schematic;
-val theorem_cmd = global_goal Proof_Context.bind_propp_schematic_cmd;
+val theorem = global_goal Proof_Context.bind_propp;
+val theorem_cmd = global_goal Proof_Context.bind_propp_cmd;
 
 fun global_qeds arg =
   end_proof true arg

--- a/src/Pure/Isar/proof_context.ML	Sun Jun 07 23:37:32 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Jun 08 14:45:31 2015 +0200
@@ -122,10 +122,6 @@
     (term list list * (indexname * term) list) * Proof.context
   val bind_propp_cmd: (string * string list) list list -> Proof.context ->
     (term list list * (indexname * term) list) * Proof.context
-  val bind_propp_schematic: (term * term list) list list -> Proof.context ->
-    (term list list * (indexname * term) list) * Proof.context
-  val bind_propp_schematic_cmd: (string * string list) list list -> Proof.context ->
-    (term list list * (indexname * term) list) * Proof.context
   val fact_tac: Proof.context -> thm list -> int -> tactic
   val some_fact_tac: Proof.context -> int -> tactic
   val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list
@@ -892,30 +888,28 @@
 
 local
 
-fun prep_propp mode prep_props raw_args ctxt =
+fun prep_propp prep_props raw_args ctxt =
   let
-    val props = prep_props (set_mode mode ctxt) (maps (map fst) raw_args);
+    val props = prep_props ctxt (maps (map fst) raw_args);
     val ctxt' = fold Variable.declare_term props ctxt;
     val patss = maps (map (prep_props (set_mode mode_pattern ctxt') o snd)) raw_args;
     val propp = unflat raw_args (props ~~ patss);
   in (propp, ctxt') end;
 
-fun gen_bind_propp mode parse_prop raw_args ctxt =
+fun gen_bind_propp parse_prop raw_args ctxt =
   let
-    val (args, ctxt') = prep_propp mode parse_prop raw_args ctxt;
+    val (args, ctxt') = prep_propp parse_prop raw_args ctxt;
     val propss = map (map fst) args;
     val binds = (maps o maps) (simult_matches ctxt') args;
   in ((propss, binds), bind_terms binds ctxt') end;
 
 in
 
-val read_propp = prep_propp mode_default Syntax.read_props;
-val cert_propp = prep_propp mode_default (map o cert_prop);
+val read_propp = prep_propp Syntax.read_props;
+val cert_propp = prep_propp (map o cert_prop);
 
-val bind_propp = gen_bind_propp mode_default (map o cert_prop);
-val bind_propp_cmd = gen_bind_propp mode_default Syntax.read_props;
-val bind_propp_schematic = gen_bind_propp mode_schematic (map o cert_prop);
-val bind_propp_schematic_cmd = gen_bind_propp mode_schematic Syntax.read_props;
+val bind_propp = gen_bind_propp (map o cert_prop);
+val bind_propp_cmd = gen_bind_propp Syntax.read_props;
 
 end;