src/HOL/Tools/function_package/fundef_package.ML
changeset 19876 11d447d5d68c
parent 19784 fa5080577da9
child 19922 984ae977f7aa
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 13 23:41:37 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 13 23:41:39 2006 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  fun fundef_afterqed congs curry_info name data names atts thmss thy =
     1.5      let
     1.6  	val (complete_thm :: compat_thms) = map hd thmss
     1.7 -	val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
     1.8 +	val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (Thm.freezeT complete_thm) (map Thm.freezeT compat_thms)
     1.9  	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, ...} = fundef_data
    1.10          val Mutual {parts, ...} = curry_info
    1.11