src/ZF/Tools/inductive_package.ML
changeset 11680 b5b96188e94c
parent 9329 d2655dc8a4b4
child 12132 1ef58b332ca9
     1.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Oct 04 15:29:22 2001 +0200
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Oct 04 15:29:37 2001 +0200
     1.3 @@ -262,7 +262,7 @@
     1.4    val intrs = ListPair.map prove_intr
     1.5  		(map (cterm_of sign1) intr_tms,
     1.6  		 map intro_tacsf (mk_disj_rls(length intr_tms)))
     1.7 -	       handle SIMPLIFIER (msg,thm) => (print_thm thm; error msg);
     1.8 +	       handle MetaSimplifier.SIMPLIFIER (msg,thm) => (print_thm thm; error msg);
     1.9  
    1.10    (********)
    1.11    val dummy = writeln "  Proving the elimination rule...";