src/HOL/Tools/inductive_realizer.ML
changeset 19617 7cb4b67d4b97
parent 19510 29fc4e5a638c
child 19806 f860b7a98445
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu May 11 19:15:16 2006 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu May 11 19:19:31 2006 +0200
     1.3 @@ -436,7 +436,7 @@
     1.4      (** add realizers to theory **)
     1.5  
     1.6      val rintr_thms = List.concat (map (fn (_, rs) => map (fn r => List.nth
     1.7 -      (#intrs ind_info, find_index_eq r intrs)) rs) rss);
     1.8 +      (#intrs ind_info, find_index (fn th => eq_thm (th, r)) intrs)) rs) rss);
     1.9      val thy4 = Library.foldl add_ind_realizer (thy3, subsets Ps);
    1.10      val thy5 = Extraction.add_realizers_i
    1.11        (map (mk_realizer thy4 vs params')