# HG changeset patch
# User krauss
# Date 1176889063 -7200
# Node ID 83099f0a9d8d8c3f2393061d9cb856a3110b6d5e
# Parent  3002683a6e0fed13b9efc57570595f2793ad7f1d
added temporary hack to avoid schematic goals in "termination".

diff -r 3002683a6e0f -r 83099f0a9d8d src/HOL/Tools/function_package/fundef_package.ML
--- 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