src/HOL/Nominal/nominal_primrec.ML

--- a/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 15 23:25:49 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 15 23:25:50 2007 +0200
@@ -388,8 +388,8 @@
     val (_, eqn_ts') = OldInductivePackage.unify_consts thy rec_ts eqn_ts
   in
     gen_primrec_i note def alt_name
-      (Option.map (map (readt TypeInfer.logicT)) invs)
-      (Option.map (readt TypeInfer.logicT) fctxt)
+      (Option.map (map (readt dummyT)) invs)
+      (Option.map (readt dummyT) fctxt)
       (names ~~ eqn_ts' ~~ atts) thy
   end;