src/HOL/Tools/primrec.ML
changeset 31786 a5ad48ae17e5
parent 31784 bd3486c57ba3
child 31902 862ae16a799d
     1.1 --- a/src/HOL/Tools/primrec.ML	Tue Jun 23 17:17:07 2009 +0200
     1.2 +++ b/src/HOL/Tools/primrec.ML	Tue Jun 23 18:10:39 2009 +0200
     1.3 @@ -239,10 +239,12 @@
     1.4      val prefix = space_implode "_" (map (Long_Name.base_name o #1) raw_defs);
     1.5      fun prove lthy defs =
     1.6        let
     1.7 +        val frees = (fold o Term.fold_aterms) (fn Free (x, _) =>
     1.8 +          if Variable.is_fixed lthy x then I else insert (op =) x | _ => I) eqs [];
     1.9          val rewrites = rec_rewrites' @ map (snd o snd) defs;
    1.10          fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
    1.11          val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
    1.12 -      in map (fn eq => [Goal.prove lthy [] [] eq tac]) eqs end;
    1.13 +      in map (fn eq => [Goal.prove lthy frees [] eq tac]) eqs end;
    1.14    in ((prefix, (fs, defs)), prove) end
    1.15    handle PrimrecError (msg, some_eqn) =>
    1.16      error ("Primrec definition error:\n" ^ msg ^ (case some_eqn