src/HOL/Tools/primrec.ML
changeset 33766 c679f05600cd
parent 33755 6dc1b67f2127
child 33963 977b94b64905
     1.1 --- a/src/HOL/Tools/primrec.ML	Thu Nov 19 14:45:56 2009 +0100
     1.2 +++ b/src/HOL/Tools/primrec.ML	Thu Nov 19 14:46:33 2009 +0100
     1.3 @@ -259,7 +259,7 @@
     1.4      val ((prefix, (fs, defs)), prove) = distill lthy fixes ts;
     1.5    in
     1.6      lthy
     1.7 -    |> fold_map (Local_Theory.define Thm.definitionK) defs
     1.8 +    |> fold_map Local_Theory.define defs
     1.9      |-> (fn defs => `(fn lthy => (prefix, prove lthy defs)))
    1.10    end;
    1.11