src/HOL/Nominal/nominal_induct.ML
changeset 23591 d32a85385e17
parent 22072 aabbf8c4de80
child 24830 a7b3ab44d993
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Thu Jul 05 20:01:26 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Thu Jul 05 20:01:28 2007 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4      val cert = Thm.cterm_of thy;
     1.5  
     1.6      val ((insts, defs), defs_ctxt) = fold_map InductMethod.add_defs def_insts ctxt |>> split_list;
     1.7 -    val atomized_defs = map (map ObjectLogic.atomize_thm) defs;
     1.8 +    val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
     1.9  
    1.10      val finish_rule =
    1.11        split_all_tuples