1.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Jun 17 18:33:11 2005 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Jun 17 18:33:12 2005 +0200
     1.3 @@ -171,7 +171,7 @@
     1.4  (* Compatibility. *)
     1.5  
     1.6  fun mk_syn thy c =
     1.7 -  if Syntax.is_identifier c andalso not (Syntax.is_keyword (Theory.syn_of thy) c) then NoSyn
     1.8 +  if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
     1.9    else Syntax.literal c
    1.10  
    1.11  fun quotename c =
    1.12 @@ -568,8 +568,7 @@
    1.13  	    case get_segment2 thyname thy of
    1.14  		SOME seg => seg
    1.15  	      | NONE => get_import_segment thy
    1.16 -	val defpath = [OS.Path.joinDirFile {dir=getenv "ISABELLE_HOME_USER",file="proofs"}]
    1.17 -	val path = space_explode ":" (getenv "PROOF_DIRS") @ defpath
    1.18 +	val path = space_explode ":" (getenv "HOL4_PROOFS")
    1.19  	fun find [] = NONE
    1.20  	  | find (p::ps) =
    1.21  	    (let
    1.22 @@ -1208,10 +1207,10 @@
    1.23      let
    1.24  	val sg = sign_of thy
    1.25  
    1.26 -	val hol4rews1 = map (transfer_sg sg) (HOL4Rewrites.get thy)
    1.27 +	val hol4rews1 = map (Thm.transfer sg) (HOL4Rewrites.get thy)
    1.28  	val hol4ss = empty_ss setmksimps single addsimps hol4rews1
    1.29      in
    1.30 -	transfer_sg sg (Simplifier.full_rewrite hol4ss (cterm_of sg t))
    1.31 +	Thm.transfer sg (Simplifier.full_rewrite hol4ss (cterm_of sg t))
    1.32      end
    1.33  
    1.34  
    1.35 @@ -2057,7 +2056,7 @@
    1.36  
    1.37  	    val sg = sign_of thy4
    1.38  	    val rew = rewrite_hol4_term (concl_of td_th) thy4
    1.39 -	    val th  = equal_elim rew (transfer_sg sg td_th)
    1.40 +	    val th  = equal_elim rew (Thm.transfer sg td_th)
    1.41  	    val c   = case HOLogic.dest_Trueprop (prop_of th) of
    1.42  			  Const("Ex",exT) $ P =>
    1.43  			  let