src/HOL/Import/proof_kernel.ML
changeset 22596 d0d2af4db18f
parent 20854 f9cf9e62d11c
child 22675 acf10be7dcca
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Apr 04 20:22:32 2007 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Apr 04 23:29:33 2007 +0200
     1.3 @@ -194,9 +194,9 @@
     1.4  
     1.5  fun simple_smart_string_of_cterm ct =
     1.6      let
     1.7 -	val {sign,t,T,...} = rep_cterm ct
     1.8 +	val {thy,t,T,...} = rep_cterm ct
     1.9  	(* Hack to avoid parse errors with Trueprop *)
    1.10 -	val ct  = (cterm_of sign (HOLogic.dest_Trueprop t)
    1.11 +	val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
    1.12  			   handle TERM _ => ct)
    1.13      in
    1.14  	quote(
    1.15 @@ -212,9 +212,9 @@
    1.16  
    1.17  fun smart_string_of_cterm ct =
    1.18      let
    1.19 -	val {sign,t,T,...} = rep_cterm ct
    1.20 +	val {thy,t,T,...} = rep_cterm ct
    1.21          (* Hack to avoid parse errors with Trueprop *)
    1.22 -	val ct  = (cterm_of sign (HOLogic.dest_Trueprop t)
    1.23 +	val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
    1.24  		   handle TERM _ => ct)
    1.25  	fun match cu = t aconv (term_of cu)
    1.26  	fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
    1.27 @@ -225,7 +225,7 @@
    1.28  	fun F n =
    1.29  	    let
    1.30  		val str = Library.setmp show_brackets false (G n string_of_cterm) ct
    1.31 -		val cu  = read_cterm sign (str,T)
    1.32 +		val cu  = read_cterm thy (str,T)
    1.33  	    in
    1.34  		if match cu
    1.35  		then quote str