src/Pure/old_goals.ML

   "Goal::prop=>prop" to avoid assumptions being returned separately.
 *)
 fun prepare_proof atomic rths chorn =
   let
       val _ = legacy_feature "Old goal command";
-      val {thy, t=horn,...} = rep_cterm chorn;
+      val thy = Thm.theory_of_cterm chorn;
+      val horn = Thm.term_of chorn;
       val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
       val (As, B) = Logic.strip_horn horn;
       val atoms = atomic andalso
             forall (fn t => not (can Logic.dest_implies t orelse can Logic.dest_all t)) As;
       val (As,B) = if atoms then ([],horn) else (As,B);

         let val state = Seq.hd (flexflex_rule state)
                         handle THM _ => state   (*smash flexflex pairs*)
             val ngoals = nprems_of state
             val ath = implies_intr_list cAs state
             val th = Goal.conclude ath
-            val {hyps,prop,thy=thy',...} = rep_thm th
+            val thy' = Thm.theory_of_thm th
+            val {hyps, prop, ...} = Thm.rep_thm th
             val final_th = standard th
         in  if not check then final_th
             else if not (eq_thy(thy,thy')) then !result_error_fn state
                 ("Theory of proof state has changed!" ^
                  thy_error (thy,thy'))

       fun statef() =
           (case Seq.pull (tac st0) of
                SOME(st,_) => st
              | _ => error ("prove_goal: tactic failed"))
   in  mkresult (check, cond_timeit (!Output.timing) "" statef)  end
-  handle e => (print_sign_exn_unit (#thy (rep_cterm chorn)) e;
+  handle e => (print_sign_exn_unit (Thm.theory_of_cterm chorn) e;
                writeln ("The exception above was raised for\n" ^
                       Display.string_of_cterm chorn); raise e);
 
 (*Two variants: one checking the result, one not.
   Neither prints runtime messages: they are for internal packages.*)