--- a/src/Pure/Isar/class.ML Mon Jun 15 08:16:08 2009 +0200
+++ b/src/Pure/Isar/class.ML Mon Jun 15 08:16:09 2009 +0200
@@ -78,7 +78,7 @@
val ((_, [thm']), _) = Variable.import_thms true [thm] empty_ctxt;
val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
- in SkipProof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
+ in Goal.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
val assm_intro = Option.map prove_assm_intro
(fst (Locale.intros_of thy class));
@@ -95,7 +95,7 @@
(Tactic.match_tac (axclass_intro :: sup_of_classes
@ loc_axiom_intros @ base_sort_trivs)
ORELSE' Tactic.assume_tac));
- val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac);
+ val of_class = Goal.prove_global thy [] [] of_class_prop (K tac);
in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;