src/Pure/old_goals.ML
changeset 32957 675c0c7e6a37
parent 32738 15bb09ca0378
child 32966 5b21661fe618
     1.1 --- a/src/Pure/old_goals.ML	Fri Oct 16 10:55:07 2009 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Sat Oct 17 00:52:37 2009 +0200
     1.3 @@ -305,7 +305,7 @@
     1.4              val th = Goal.conclude ath
     1.5              val thy' = Thm.theory_of_thm th
     1.6              val {hyps, prop, ...} = Thm.rep_thm th
     1.7 -            val final_th = standard th
     1.8 +            val final_th = Drule.standard th
     1.9          in  if not check then final_th
    1.10              else if not (Theory.eq_thy(thy,thy')) then !result_error_fn state
    1.11                  ("Theory of proof state has changed!" ^
    1.12 @@ -512,7 +512,7 @@
    1.13              0 => thm
    1.14            | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
    1.15    in
    1.16 -    standard (implies_intr_list As
    1.17 +    Drule.standard (implies_intr_list As
    1.18        (check (Seq.pull (EVERY (f asms) (trivial B)))))
    1.19    end;
    1.20