src/Pure/Isar/class.ML
changeset 39438 c5ece2a7a86e
parent 39378 df86b1b4ce10
child 39557 fe5722fce758
     1.1 --- a/src/Pure/Isar/class.ML	Thu Sep 16 15:32:24 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Sep 16 15:37:12 2010 +0200
     1.3 @@ -630,7 +630,8 @@
     1.4    end;
     1.5  
     1.6  fun default_intro_tac ctxt [] =
     1.7 -      intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
     1.8 +      COND Thm.no_prems no_tac
     1.9 +        (intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [])
    1.10    | default_intro_tac _ _ = no_tac;
    1.11  
    1.12  fun default_tac rules ctxt facts =