--- a/src/HOL/Tools/primrec.ML Tue Jun 23 17:17:07 2009 +0200
+++ b/src/HOL/Tools/primrec.ML Tue Jun 23 18:10:39 2009 +0200
@@ -239,10 +239,12 @@
val prefix = space_implode "_" (map (Long_Name.base_name o #1) raw_defs);
fun prove lthy defs =
let
+ val frees = (fold o Term.fold_aterms) (fn Free (x, _) =>
+ if Variable.is_fixed lthy x then I else insert (op =) x | _ => I) eqs [];
val rewrites = rec_rewrites' @ map (snd o snd) defs;
fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
- in map (fn eq => [Goal.prove lthy [] [] eq tac]) eqs end;
+ in map (fn eq => [Goal.prove lthy frees [] eq tac]) eqs end;
in ((prefix, (fs, defs)), prove) end
handle PrimrecError (msg, some_eqn) =>
error ("Primrec definition error:\n" ^ msg ^ (case some_eqn