src/HOL/Tools/primrec_package.ML

                     (list_comb (Const (rec_name, dummyT),
                                 fs @ map Bound (0 ::(length ls downto 1))))
     val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
     val def_prop =
       singleton (ProofContext.infer_types (ProofContext.init thy))
-        (Logic.mk_equals (Const (fname, dummyT), rhs), propT) |> #1;
+        (Logic.mk_equals (Const (fname, dummyT), rhs));
   in (def_name, def_prop) end;
 
 
 (* find datatypes which contain all datatypes in tnames' *)