src/HOLCF/Tools/fixrec.ML
changeset 33766 c679f05600cd
parent 33726 0878aecbf119
child 35525 fa231b86cb1e
--- a/src/HOLCF/Tools/fixrec.ML	Thu Nov 19 14:45:56 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML	Thu Nov 19 14:46:33 2009 +0100
@@ -209,9 +209,8 @@
       | defs (l::[]) r = [one_def l r]
       | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
     val fixdefs = defs lhss fixpoint;
-    val define_all = fold_map (Local_Theory.define Thm.definitionK);
     val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
-      |> define_all (map (apfst fst) fixes ~~ fixdefs);
+      |> fold_map Local_Theory.define (map (apfst fst) fixes ~~ fixdefs);
     fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
     val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms);
     val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT);