src/HOL/Nominal/nominal_induct.ML

--- a/src/HOL/Nominal/nominal_induct.ML	Thu Jul 05 20:01:26 2007 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Thu Jul 05 20:01:28 2007 +0200
@@ -88,7 +88,7 @@
     val cert = Thm.cterm_of thy;
 
     val ((insts, defs), defs_ctxt) = fold_map InductMethod.add_defs def_insts ctxt |>> split_list;
-    val atomized_defs = map (map ObjectLogic.atomize_thm) defs;
+    val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
 
     val finish_rule =
       split_all_tuples