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