--- a/src/HOL/Tools/primrec_package.ML Thu Sep 24 17:16:06 1998 +0200
+++ b/src/HOL/Tools/primrec_package.ML Thu Sep 24 17:17:14 1998 +0200
@@ -221,7 +221,7 @@
(if eq_set (names1, names2) then Theory.add_defs_i defs'
else primrec_err ("functions " ^ commas names2 ^
"\nare not mutually recursive"));
- val rewrites = (map meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs');
+ val rewrites = (map mk_meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs');
val _ = writeln ("Proving equations for primrec function(s)\n" ^
commas names1 ^ " ...");
val char_thms = map (fn t => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t)