equal
deleted
inserted
replaced
245 let |
245 let |
246 val frees = fold (Variable.add_free_names ctxt) eqs []; |
246 val frees = fold (Variable.add_free_names ctxt) eqs []; |
247 val rewrites = rec_rewrites' @ map (snd o snd) defs; |
247 val rewrites = rec_rewrites' @ map (snd o snd) defs; |
248 in |
248 in |
249 map (fn eq => Goal.prove ctxt frees [] eq |
249 map (fn eq => Goal.prove ctxt frees [] eq |
250 (fn {context = ctxt', ...} => EVERY [rewrite_goals_tac ctxt' rewrites, rtac refl 1])) eqs |
250 (fn {context = ctxt', ...} => |
|
251 EVERY [rewrite_goals_tac ctxt' rewrites, resolve_tac [refl] 1])) eqs |
251 end; |
252 end; |
252 in ((prefix, (fs, defs)), prove) end |
253 in ((prefix, (fs, defs)), prove) end |
253 handle PrimrecError (msg, some_eqn) => |
254 handle PrimrecError (msg, some_eqn) => |
254 error ("Primrec definition error:\n" ^ msg ^ |
255 error ("Primrec definition error:\n" ^ msg ^ |
255 (case some_eqn of |
256 (case some_eqn of |