src/Pure/Isar/class_declaration.ML
changeset 52788 da1fdbfebd39
parent 52732 b4da1f2ec73f
child 54740 91f54d386680
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Tue Jul 30 12:07:14 2013 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Tue Jul 30 15:09:25 2013 +0200
     1.3 @@ -314,7 +314,6 @@
     1.4      |> Expression.add_locale I b (Binding.qualify true "class" b) supexpr elems
     1.5      |> snd |> Local_Theory.exit_global
     1.6      |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
     1.7 -    ||> Theory.checkpoint
     1.8      |-> (fn (param_map, params, assm_axiom) =>
     1.9         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
    1.10      #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>