# HG changeset patch
# User wenzelm
# Date 1284644232 -7200
# Node ID c5ece2a7a86eee42f377176babb6c4672355593c
# Parent  8c23c61c6d5c2cd3646c2470378eb1aa86cf4f3e
Isar "default" step needs to fail for solved problems, for clear distinction of '.' and '..' for example -- amending lapse introduced in 9de4d64eee3b (April 2004);

diff -r 8c23c61c6d5c -r c5ece2a7a86e src/HOL/Power.thy
--- a/src/HOL/Power.thy	Thu Sep 16 15:32:24 2010 +0200
+++ b/src/HOL/Power.thy	Thu Sep 16 15:37:12 2010 +0200
@@ -29,7 +29,7 @@
 context monoid_mult
 begin
 
-subclass power ..
+subclass power .
 
 lemma power_one [simp]:
   "1 ^ n = 1"
diff -r 8c23c61c6d5c -r c5ece2a7a86e src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Thu Sep 16 15:32:24 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Thu Sep 16 15:37:12 2010 +0200
@@ -791,7 +791,7 @@
     "k < l \<Longrightarrow> divmod_rel k l 0 k"
   | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
 
-code_pred divmod_rel ..
+code_pred divmod_rel .
 thm divmod_rel.equation
 value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
 
diff -r 8c23c61c6d5c -r c5ece2a7a86e src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Sep 16 15:32:24 2010 +0200
+++ b/src/Pure/Isar/class.ML	Thu Sep 16 15:37:12 2010 +0200
@@ -630,7 +630,8 @@
   end;
 
 fun default_intro_tac ctxt [] =
-      intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
+      COND Thm.no_prems no_tac
+        (intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [])
   | default_intro_tac _ _ = no_tac;
 
 fun default_tac rules ctxt facts =