--- a/src/Pure/Isar/obtain.ML Fri Dec 17 16:25:21 2010 +0100
+++ b/src/Pure/Isar/obtain.ML Fri Dec 17 17:08:56 2010 +0100
@@ -193,7 +193,7 @@
val rule =
(case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
- | SOME th => check_result ctxt thesis (MetaSimplifier.norm_hhf (Goal.conclude th)));
+ | SOME th => check_result ctxt thesis (Raw_Simplifier.norm_hhf (Goal.conclude th)));
val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
@@ -299,7 +299,7 @@
val goal = Var (("guess", 0), propT);
fun print_result ctxt' (k, [(s, [_, th])]) =
Proof_Display.print_results int ctxt' (k, [(s, [th])]);
- val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
+ val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #>
(fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
fun after_qed [[_, res]] =
Proof.end_block #> guess_context (check_result ctxt thesis res);