diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Tools/induct.ML	Wed Jun 08 15:56:57 2011 +0200
@@ -590,7 +590,7 @@
         Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
         |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
       end
-  end handle Subscript => Seq.empty;
+  end handle General.Subscript => Seq.empty;
 
 end;