src/Pure/Isar/proof.ML

   val map_context: (context -> context) -> state -> state
   val warn_extra_tfrees: state -> state -> state
   val put_thms: string * thm list option -> state -> state
   val the_facts: state -> thm list
   val the_fact: state -> thm
+  val put_facts: thm list option -> state -> state
   val assert_forward: state -> state
   val assert_chain: state -> state
   val assert_forward_or_chain: state -> state
   val assert_backward: state -> state
   val assert_no_chain: state -> state

   val defer: int option -> state -> state Seq.seq
   val prefer: int -> state -> state Seq.seq
   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))) ->
-   string -> (context * thm list -> thm list list -> theory -> theory) -> string option ->
-   string * 'a list -> ((string * 'a list) * 'b) list -> context -> state
+    (theory -> 'a -> theory attribute) ->
+    (context * 'b list -> context * (term list list * (context -> context))) ->
+    string -> (context * thm list -> thm list list -> theory -> theory) -> string option ->
+    string * 'a list -> ((string * 'a list) * 'b) list -> context -> state
   val global_qed: Method.text option * bool -> state -> theory * context
   val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq
   val local_default_proof: state -> state Seq.seq
   val local_immediate_proof: state -> state Seq.seq
   val local_done_proof: state -> state Seq.seq

       err (Pretty.string_of (Pretty.chunks
         (pretty_goals_local ctxt "" (true, ! show_main_goal) (! Display.goals_limit) goal @
           [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))));
 
     val {hyps, thy, ...} = Thm.rep_thm goal;
-    val casms = List.concat (map #1 (ProofContext.assumptions_of ctxt));
-    val bad_hyps = fold (remove (fn (asm, hyp) => Thm.term_of asm aconv hyp)) casms hyps;
+    val bad_hyps = fold (remove (op aconv)) (ProofContext.assms_of ctxt) hyps;
 
     val th = goal RS Drule.rev_triv_goal;
     val ths = Drule.conj_elim_precise (length props) th
       handle THM _ => err "Main goal structure corrupted";
   in

     val (names_attss, propp) = split_list (Attrib.map_specs prep_att stmt);
     val (names, attss) = split_list names_attss;
   in ((names, attss), propp) end;
 
 fun goal_names target name names =
-  (case target of NONE => "" | SOME loc => " (in " ^ loc ^ ")") ^
+  (case target of NONE => "" | SOME "" => "" | SOME loc => " (in " ^ loc ^ ")") ^
   (if name = "" then "" else " " ^ name) ^
   (case filter_out (equal "") names of [] => ""
   | nms => " " ^ enclose "(" ")" (space_implode " and " (Library.take (7, nms) @
       (if length nms > 7 then ["..."] else []))));
 

     |> K chaining ? (`the_facts #-> using_facts)
     |> put_facts NONE
     |> open_block
     |> put_goal NONE
     |> enter_backward
+    |> K (null props) ? (refine (Method.Basic Method.assumption) #> Seq.hd)
   end;
 
 fun generic_qed state =
   let
     val (goal_ctxt, {statement = (_, stmt), using, goal, after_qed}) = current_goal state;

       Seq.lifts (#1 after_qed raw_results) results));
 
 
 (* 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
     val thy = ProofContext.theory_of ctxt;
     val thy_ctxt = ProofContext.init thy;
 
     val atts = map (prep_att thy) raw_atts;
     val ((names, attss), propp) = prep_names (prep_att thy) stmt;
 
-    fun after_qed' raw_results results =
-      (map o map) (ProofContext.export_standard ctxt thy_ctxt
-        #> Drule.strip_shyps_warning) results
-      |> (fn res => global_results kind ((names ~~ attss) ~~ res))
+    fun store_results prfx res =
+      K (prfx <> "") ? (Sign.add_path prfx #> Sign.no_base_names)
+      #> global_results kind ((names ~~ attss) ~~ res)
       #-> (fn res' =>
         (print_results thy_ctxt ((kind, name), res') : unit;
           #2 o global_results kind [((name, atts), List.concat (map #2 res'))]))
+      #> Sign.restore_naming thy;
+
+    fun after_qed' raw_results results =
+      (case target of NONE => I
+      | SOME prfx => store_results (NameSpace.base prfx)
+          (map (map (ProofContext.export_standard ctxt thy_ctxt
+            #> Drule.strip_shyps_warning)) results))
       #> after_qed raw_results results;
-
-    val prepp' = prepp #> auto_fix;
   in
     init ctxt
-    |> generic_goal prepp' (kind ^ goal_names target name names)
+    |> generic_goal (prepp #> ProofContext.auto_fix) (kind ^ goal_names target name names)
       (K (K Seq.single), after_qed') propp
   end;
 
 fun check_result msg state sq =
   (case Seq.pull sq of