src/Pure/Isar/class.ML
changeset 31634 cb3bb7f79792
parent 30764 3e3e7aa0cc7a
child 31637 e1223f58ea9b
     1.1 --- a/src/Pure/Isar/class.ML	Sun Jun 14 17:20:19 2009 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sun Jun 14 17:20:19 2009 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4          val ((_, [thm']), _) = Variable.import_thms true [thm] empty_ctxt;
     1.5          val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
     1.6          val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
     1.7 -      in Goal.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
     1.8 +      in SkipProof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
     1.9      val assm_intro = Option.map prove_assm_intro
    1.10        (fst (Locale.intros_of thy class));
    1.11  
    1.12 @@ -95,7 +95,7 @@
    1.13        (Tactic.match_tac (axclass_intro :: sup_of_classes
    1.14           @ loc_axiom_intros @ base_sort_trivs)
    1.15             ORELSE' Tactic.assume_tac));
    1.16 -    val of_class = Goal.prove_global thy [] [] of_class_prop (K tac);
    1.17 +    val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac);
    1.18  
    1.19    in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
    1.20