diff -r 4e603046e539 -r 9deaf32c83be src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Sep 16 14:44:52 2005 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Sep 16 14:46:31 2005 +0200
@@ -83,12 +83,20 @@
   val apply: Method.text -> state -> state Seq.seq
   val apply_end: Method.text -> state -> state Seq.seq
   val goal_names: string option -> string -> string list -> string
+  val generic_goal:
+   (context * 'a -> context * (term list list * (context -> context))) ->
+   string ->
+   (context * thm list -> thm list list -> state -> state Seq.seq) *
+   (context * thm list -> thm list list -> theory -> theory) ->
+   'a -> state -> state
   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     (theory -> 'a -> context attribute) ->
     (context * 'b list -> context * (term list list * (context -> context))) ->
     string -> (context * thm list -> thm list list -> state -> state Seq.seq) ->
     ((string * 'a list) * 'b) list -> state -> state
   val local_qed: Method.text option * bool -> state -> state Seq.seq
+  val auto_fix: context * (term list list * 'a) ->
+    context * (term list list * 'a)
   val global_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
    (theory -> 'a -> theory attribute) ->
    (context * 'b list -> context * (term list list * (context -> context))) ->
@@ -832,6 +840,9 @@
 
 (* global goals *)
 
+fun auto_fix (ctxt, (propss, after_ctxt)) =
+  (ctxt |> ProofContext.fix_frees (List.concat propss), (propss, after_ctxt));
+
 fun global_goal print_results prep_att prepp
     kind after_qed target (name, raw_atts) stmt ctxt =
   let
@@ -850,8 +861,7 @@
           #2 o global_results kind [((name, atts), List.concat (map #2 res'))]))
       #> after_qed raw_results results;
 
-    val prepp' = prepp #> (fn (ctxt, (propss, after_ctxt)) =>
-      (ctxt |> ProofContext.fix_frees (List.concat propss), (propss, after_ctxt)));
+    val prepp' = prepp #> auto_fix;
   in
     init ctxt
     |> generic_goal prepp' (kind ^ goal_names target name names)