added temporary hack to avoid schematic goals in "termination".

--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Apr 18 11:14:09 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Apr 18 11:37:43 2007 +0200
@@ -140,6 +140,7 @@
       val FundefCtxData { add_simps, psimps, pinducts, ... } = data
 
       val totality = Goal.close_result totality
+                       |> Thm.varifyT (* FIXME ! *)
 
       val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
 
@@ -167,6 +168,7 @@
         val FundefCtxData {termination, R, ...} = data
         val domT = domain_type (fastype_of R)
         val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
+                     |> Type.freeze (* FIXME ! *)
     in
       lthy
         |> ProofContext.note_thmss_i "" [(("", [ContextRules.rule_del]), [([allI], [])])] |> snd