unfold_locales now part of default tactic
authorhaftmann
Fri Mar 28 22:01:56 2008 +0100 (2008-03-28)
changeset 26470e44d24620515
parent 26469 6deb216d726f
child 26471 f4c956461353
unfold_locales now part of default tactic
src/Provers/classical.ML
src/Pure/Isar/class.ML
     1.1 --- a/src/Provers/classical.ML	Fri Mar 28 22:01:04 2008 +0100
     1.2 +++ b/src/Provers/classical.ML	Fri Mar 28 22:01:56 2008 +0100
     1.3 @@ -1019,7 +1019,7 @@
     1.4  
     1.5  fun default_tac rules ctxt cs facts =
     1.6    HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
     1.7 -  Class.default_intro_classes_tac facts;
     1.8 +  Class.default_intro_tac ctxt facts;
     1.9  
    1.10  in
    1.11    val rule = METHOD_CLASET' o rule_tac;
     2.1 --- a/src/Pure/Isar/class.ML	Fri Mar 28 22:01:04 2008 +0100
     2.2 +++ b/src/Pure/Isar/class.ML	Fri Mar 28 22:01:56 2008 +0100
     2.3 @@ -21,7 +21,7 @@
     2.4    val refresh_syntax: class -> Proof.context -> Proof.context
     2.5  
     2.6    val intro_classes_tac: thm list -> tactic
     2.7 -  val default_intro_classes_tac: thm list -> tactic
     2.8 +  val default_intro_tac: Proof.context -> thm list -> tactic
     2.9    val prove_subclass: class * class -> thm -> theory -> theory
    2.10  
    2.11    val class_prefix: string -> string
    2.12 @@ -388,12 +388,13 @@
    2.13      Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
    2.14    end;
    2.15  
    2.16 -fun default_intro_classes_tac [] = intro_classes_tac []
    2.17 -  | default_intro_classes_tac _ = no_tac;
    2.18 +fun default_intro_tac ctxt [] =
    2.19 +      intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
    2.20 +  | default_intro_tac _ _ = no_tac;
    2.21  
    2.22  fun default_tac rules ctxt facts =
    2.23    HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
    2.24 -    default_intro_classes_tac facts;
    2.25 +    default_intro_tac ctxt facts;
    2.26  
    2.27  val _ = Context.>> (Context.map_theory
    2.28    (Method.add_methods