src/Pure/Isar/class.ML
changeset 26470 e44d24620515
parent 26463 9283b4185fdf
child 26518 3db6a46d8460
     1.1 --- a/src/Pure/Isar/class.ML	Fri Mar 28 22:01:04 2008 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Mar 28 22:01:56 2008 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4    val refresh_syntax: class -> Proof.context -> Proof.context
     1.5  
     1.6    val intro_classes_tac: thm list -> tactic
     1.7 -  val default_intro_classes_tac: thm list -> tactic
     1.8 +  val default_intro_tac: Proof.context -> thm list -> tactic
     1.9    val prove_subclass: class * class -> thm -> theory -> theory
    1.10  
    1.11    val class_prefix: string -> string
    1.12 @@ -388,12 +388,13 @@
    1.13      Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
    1.14    end;
    1.15  
    1.16 -fun default_intro_classes_tac [] = intro_classes_tac []
    1.17 -  | default_intro_classes_tac _ = no_tac;
    1.18 +fun default_intro_tac ctxt [] =
    1.19 +      intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
    1.20 +  | default_intro_tac _ _ = no_tac;
    1.21  
    1.22  fun default_tac rules ctxt facts =
    1.23    HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
    1.24 -    default_intro_classes_tac facts;
    1.25 +    default_intro_tac ctxt facts;
    1.26  
    1.27  val _ = Context.>> (Context.map_theory
    1.28    (Method.add_methods