src/Pure/Isar/class.ML
changeset 36674 d95f39448121
parent 36672 bd7f659f7de5
child 36745 403585a89772
     1.1 --- a/src/Pure/Isar/class.ML	Wed May 05 09:24:41 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed May 05 09:24:42 2010 +0200
     1.3 @@ -74,7 +74,10 @@
     1.4      fun prove_assm_intro thm =
     1.5        let
     1.6          val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
     1.7 -        val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
     1.8 +        val const_eq_morph = case eq_morph
     1.9 +         of SOME eq_morph => const_morph $> eq_morph
    1.10 +          | NONE => const_morph
    1.11 +        val thm'' = Morphism.thm const_eq_morph thm';
    1.12          val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
    1.13        in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
    1.14      val assm_intro = Option.map prove_assm_intro
    1.15 @@ -290,7 +293,9 @@
    1.16      |-> (fn (param_map, params, assm_axiom) =>
    1.17         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
    1.18      #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
    1.19 -       Locale.add_registration (class, base_morph $> eq_morph (*FIXME duplication*)) (SOME (eq_morph, true)) export_morph
    1.20 +       Locale.add_registration (class, case eq_morph of SOME eq_morph => base_morph $> eq_morph | NONE => base_morph)
    1.21 +         (*FIXME should avoid modification of base morphism, but then problem with sublocale linorder < distrib_lattice*)
    1.22 +         (Option.map (rpair true) eq_morph) export_morph
    1.23      #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
    1.24      |> Theory_Target.init (SOME class)
    1.25      |> pair class