src/Pure/old_goals.ML
changeset 26626 c6231d64d264
parent 26429 1afbc0139b1b
child 26653 60e0cf6bef89
     1.1 --- a/src/Pure/old_goals.ML	Thu Apr 10 20:54:18 2008 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Sat Apr 12 17:00:35 2008 +0200
     1.3 @@ -151,7 +151,8 @@
     1.4  fun prepare_proof atomic rths chorn =
     1.5    let
     1.6        val _ = legacy_feature "Old goal command";
     1.7 -      val {thy, t=horn,...} = rep_cterm chorn;
     1.8 +      val thy = Thm.theory_of_cterm chorn;
     1.9 +      val horn = Thm.term_of chorn;
    1.10        val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
    1.11        val (As, B) = Logic.strip_horn horn;
    1.12        val atoms = atomic andalso
    1.13 @@ -170,7 +171,8 @@
    1.14              val ngoals = nprems_of state
    1.15              val ath = implies_intr_list cAs state
    1.16              val th = Goal.conclude ath
    1.17 -            val {hyps,prop,thy=thy',...} = rep_thm th
    1.18 +            val thy' = Thm.theory_of_thm th
    1.19 +            val {hyps, prop, ...} = Thm.rep_thm th
    1.20              val final_th = standard th
    1.21          in  if not check then final_th
    1.22              else if not (eq_thy(thy,thy')) then !result_error_fn state
    1.23 @@ -229,7 +231,7 @@
    1.24                 SOME(st,_) => st
    1.25               | _ => error ("prove_goal: tactic failed"))
    1.26    in  mkresult (check, cond_timeit (!Output.timing) "" statef)  end
    1.27 -  handle e => (print_sign_exn_unit (#thy (rep_cterm chorn)) e;
    1.28 +  handle e => (print_sign_exn_unit (Thm.theory_of_cterm chorn) e;
    1.29                 writeln ("The exception above was raised for\n" ^
    1.30                        Display.string_of_cterm chorn); raise e);
    1.31