# HG changeset patch # User haftmann # Date 1245253356 -7200 # Node ID 8b3dac635907302ee9a587ae3fb794cb282de517 # Parent cc37bf07f9bb375cd372b8b50a9b1db2f28972b5 skip_proof where appropriate diff -r cc37bf07f9bb -r 8b3dac635907 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Jun 17 15:41:49 2009 +0200 +++ b/src/Pure/Isar/class.ML Wed Jun 17 17:42:36 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 Goal.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end; + in SkipProof.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 = Goal.prove_global thy [] [] of_class_prop (K tac); + val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac); in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end; @@ -281,6 +281,7 @@ |> Expression.add_locale bname Binding.empty supexpr elems |> snd |> LocalTheory.exit_global |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax + ||> Theory.checkpoint |-> (fn (param_map, params, assm_axiom) => `(fn thy => calculate thy class sups base_sort param_map assm_axiom) #-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>