--- a/src/ZF/Tools/induct_tacs.ML Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Mon Dec 20 16:44:33 2010 +0100
@@ -118,7 +118,7 @@
fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
let
(*analyze the LHS of a case equation to get a constructor*)
- fun const_of (Const(@{const_name "op ="}, _) $ (_ $ c) $ _) = c
+ fun const_of (Const(@{const_name IFOL.eq}, _) $ (_ $ c) $ _) = c
| const_of eqn = error ("Ill-formed case equation: " ^
Syntax.string_of_term_global thy eqn);