src/Tools/induct.ML
changeset 43278 1fbdcebb364b
parent 42488 4638622bcaa1
child 43326 47cf4bc789aa
     1.1 --- a/src/Tools/induct.ML	Wed Jun 08 15:39:55 2011 +0200
     1.2 +++ b/src/Tools/induct.ML	Wed Jun 08 15:56:57 2011 +0200
     1.3 @@ -590,7 +590,7 @@
     1.4          Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
     1.5          |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
     1.6        end
     1.7 -  end handle Subscript => Seq.empty;
     1.8 +  end handle General.Subscript => Seq.empty;
     1.9  
    1.10  end;
    1.11