src/Pure/Isar/class.ML
changeset 27684 f45fd1159a4b
parent 27281 b457537e789a
child 27690 24738db98d34
     1.1 --- a/src/Pure/Isar/class.ML	Fri Jul 25 12:03:36 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Jul 25 12:03:37 2008 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4  
     1.5    val intro_classes_tac: thm list -> tactic
     1.6    val default_intro_tac: Proof.context -> thm list -> tactic
     1.7 -  val prove_subclass: class * class -> thm -> theory -> theory
     1.8 +  val prove_subclass: class * class -> thm option -> theory -> theory
     1.9  
    1.10    val class_prefix: string -> string
    1.11    val is_class: theory -> class -> bool
    1.12 @@ -338,7 +338,7 @@
    1.13    in
    1.14      thy
    1.15      |> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN)
    1.16 -    |> PureThy.note Thm.internalK (AxClass.introN, this_intro)
    1.17 +    |> PureThy.store_thm (AxClass.introN, this_intro)
    1.18      |> snd
    1.19      |> Sign.restore_naming thy
    1.20      |> pair (morphism, axiom, assm_intro, of_class)
    1.21 @@ -362,15 +362,19 @@
    1.22      |> fold2 add_constraint (map snd consts) constraints
    1.23    end;
    1.24  
    1.25 -fun prove_subclass (sub, sup) thm thy =
    1.26 +fun prove_subclass (sub, sup) some_thm thy =
    1.27    let
    1.28      val of_class = (#of_class o the_class_data thy) sup;
    1.29 -    val intro = Drule.standard' (of_class OF [Drule.standard' thm]);
    1.30 -    val classrel = intro OF (the_list o #axiom o the_class_data thy) sub;
    1.31 +    val intro = case some_thm
    1.32 +     of SOME thm => Drule.standard' (of_class OF [Drule.standard' thm])
    1.33 +      | NONE => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
    1.34 +          ([], [sub])], []) of_class;
    1.35 +    val classrel = (intro OF (the_list o #axiom o the_class_data thy) sub)
    1.36 +      |> Thm.close_derivation;
    1.37    in
    1.38      thy
    1.39      |> AxClass.add_classrel classrel
    1.40 -    |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac [thm]))
    1.41 +    |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac (the_list some_thm)))
    1.42           I (sub, Locale.Locale sup)
    1.43      |> ClassData.map (Graph.add_edge (sub, sup))
    1.44    end;
    1.45 @@ -557,7 +561,7 @@
    1.46        prep_spec thy raw_supclasses raw_elems;
    1.47    in
    1.48      thy
    1.49 -    |> Locale.add_locale_i (SOME "") bname mergeexpr elems
    1.50 +    |> Locale.add_locale_i "" bname mergeexpr elems
    1.51      |> snd
    1.52      |> ProofContext.theory_of
    1.53      |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
    1.54 @@ -602,7 +606,7 @@
    1.55      ||>> get_axiom
    1.56      |-> (fn (def, def') => class_interpretation class [def] [Thm.prop_of def]
    1.57        #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
    1.58 -      #> PureThy.note Thm.internalK (c ^ "_raw", def')
    1.59 +      #> PureThy.store_thm (c ^ "_raw", def')
    1.60        #> snd)
    1.61      |> Sign.restore_naming thy
    1.62      |> Sign.add_const_constraint (c', SOME ty')