src/Pure/Isar/class_declaration.ML
changeset 46856 28909eecdf5b
parent 45433 4283f3a57cf5
child 46922 3717f3878714
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Sat Mar 10 16:49:34 2012 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Sat Mar 10 17:07:10 2012 +0100
     1.3 @@ -74,13 +74,12 @@
     1.4          val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
     1.5          val const_eq_morph =
     1.6            (case eq_morph of
     1.7 -             SOME eq_morph => const_morph $> eq_morph
     1.8 +            SOME eq_morph => const_morph $> eq_morph
     1.9            | NONE => const_morph);
    1.10          val thm'' = Morphism.thm const_eq_morph thm';
    1.11          val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
    1.12        in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
    1.13 -    val assm_intro = Option.map prove_assm_intro
    1.14 -      (fst (Locale.intros_of thy class));
    1.15 +    val assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
    1.16  
    1.17      (* of_class *)
    1.18      val of_class_prop_concl = Logic.mk_of_class (aT, class);