src/Pure/Isar/obtain.ML

 
     val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
     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;
     val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
     val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';

       end;
 
     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);
   in
     state