added temporary hack to avoid schematic goals in "termination".
authorkrauss
Wed Apr 18 11:37:43 2007 +0200 (2007-04-18)
changeset 2272583099f0a9d8d
parent 22724 3002683a6e0f
child 22726 11e01dc78377
added temporary hack to avoid schematic goals in "termination".
src/HOL/Tools/function_package/fundef_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Apr 18 11:14:09 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Apr 18 11:37:43 2007 +0200
     1.3 @@ -140,6 +140,7 @@
     1.4        val FundefCtxData { add_simps, psimps, pinducts, ... } = data
     1.5  
     1.6        val totality = Goal.close_result totality
     1.7 +                       |> Thm.varifyT (* FIXME ! *)
     1.8  
     1.9        val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
    1.10  
    1.11 @@ -167,6 +168,7 @@
    1.12          val FundefCtxData {termination, R, ...} = data
    1.13          val domT = domain_type (fastype_of R)
    1.14          val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
    1.15 +                     |> Type.freeze (* FIXME ! *)
    1.16      in
    1.17        lthy
    1.18          |> ProofContext.note_thmss_i "" [(("", [ContextRules.rule_del]), [([allI], [])])] |> snd