refer to HOL4_PROOFS setting;
accomodate identification of type Sign.sg and theory;
--- a/src/HOL/Import/proof_kernel.ML Fri Jun 17 18:33:11 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Jun 17 18:33:12 2005 +0200
@@ -171,7 +171,7 @@
(* Compatibility. *)
fun mk_syn thy c =
- if Syntax.is_identifier c andalso not (Syntax.is_keyword (Theory.syn_of thy) c) then NoSyn
+ if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
else Syntax.literal c
fun quotename c =
@@ -568,8 +568,7 @@
case get_segment2 thyname thy of
SOME seg => seg
| NONE => get_import_segment thy
- val defpath = [OS.Path.joinDirFile {dir=getenv "ISABELLE_HOME_USER",file="proofs"}]
- val path = space_explode ":" (getenv "PROOF_DIRS") @ defpath
+ val path = space_explode ":" (getenv "HOL4_PROOFS")
fun find [] = NONE
| find (p::ps) =
(let
@@ -1208,10 +1207,10 @@
let
val sg = sign_of thy
- val hol4rews1 = map (transfer_sg sg) (HOL4Rewrites.get thy)
+ val hol4rews1 = map (Thm.transfer sg) (HOL4Rewrites.get thy)
val hol4ss = empty_ss setmksimps single addsimps hol4rews1
in
- transfer_sg sg (Simplifier.full_rewrite hol4ss (cterm_of sg t))
+ Thm.transfer sg (Simplifier.full_rewrite hol4ss (cterm_of sg t))
end
@@ -2057,7 +2056,7 @@
val sg = sign_of thy4
val rew = rewrite_hol4_term (concl_of td_th) thy4
- val th = equal_elim rew (transfer_sg sg td_th)
+ val th = equal_elim rew (Thm.transfer sg td_th)
val c = case HOLogic.dest_Trueprop (prop_of th) of
Const("Ex",exT) $ P =>
let