src/HOL/Tools/function_package/fundef_prep.ML
changeset 19876 11d447d5d68c
parent 19781 c62720b20e9a
child 19922 984ae977f7aa
     1.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Tue Jun 13 23:41:37 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Tue Jun 13 23:41:39 2006 +0200
     1.3 @@ -91,7 +91,7 @@
     1.4  	val localize = instantiate ([], cvqs ~~ cqs) 
     1.5  					   #> fold implies_elim_swp ags
     1.6  
     1.7 -	val GI = freezeT GI
     1.8 +	val GI = Thm.freezeT GI
     1.9  	val lGI = localize GI
    1.10  
    1.11  	val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [] o var_to_free) (term_vars (prop_of GI))
    1.12 @@ -100,7 +100,7 @@
    1.13  	    let
    1.14  		fun mk_var0 (v,T) = Var ((v,0),T)
    1.15  
    1.16 -		val RI = freezeT RI
    1.17 +		val RI = Thm.freezeT RI
    1.18  		val lRI = localize RI
    1.19  		val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI
    1.20  		val plRI = prop_of lRI
    1.21 @@ -295,4 +295,4 @@
    1.22  
    1.23  
    1.24  
    1.25 -end
    1.26 \ No newline at end of file
    1.27 +end