--- a/src/Pure/old_goals.ML Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/old_goals.ML Sun Feb 07 19:33:34 2010 +0100
@@ -305,7 +305,7 @@
val th = Goal.conclude ath
val thy' = Thm.theory_of_thm th
val {hyps, prop, ...} = Thm.rep_thm th
- val final_th = Drule.standard th
+ val final_th = Drule.export_without_context th
in if not check then final_th
else if not (Theory.eq_thy(thy,thy')) then !result_error_fn state
("Theory of proof state has changed!" ^
@@ -512,7 +512,7 @@
0 => thm
| i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
in
- Drule.standard (implies_intr_list As
+ Drule.export_without_context (implies_intr_list As
(check (Seq.pull (EVERY (f asms) (trivial B)))))
end;