Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/tactical.ML
changeset 43278 1fbdcebb364b
parent 39125 f45d332a90e3
child 46463 3d0629a9ffca 
--- a/src/Pure/tactical.ML	Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Pure/tactical.ML	Wed Jun 08 15:56:57 2011 +0200
@@ -354,7 +354,7 @@
             orelse
              not (Pattern.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
     in  Seq.filter diff (tac i st)  end
-    handle Subscript => Seq.empty  (*no subgoal i*);
+    handle General.Subscript => Seq.empty  (*no subgoal i*);
 
 (*Returns all states where some subgoals have been solved.  For
   subgoal-based tactics this means subgoal i has been solved
isabelle