src/HOL/Tools/function_package/fundef_package.ML
changeset 22725 83099f0a9d8d
parent 22668 8183ee579232
child 22733 0b14bb35be90
     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