--- a/src/FOLP/simp.ML Tue Jan 18 15:57:40 1994 +0100
+++ b/src/FOLP/simp.ML Tue Jan 18 16:37:12 1994 +0100
@@ -436,7 +436,7 @@
are represented by rules, generalized over their parameters*)
fun add_asms(ss,thm,a,anet,ats,cs) =
let val As = strip_varify(nth_subgoal i thm, a, []);
- val thms = map (trivial o Sign.cterm_of(#sign(rep_thm(thm))))As;
+ val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
val new_rws = flat(map mk_rew_rules thms);
val rwrls = map mk_trans (flat(map mk_rew_rules thms));
val anet' = foldr lhs_insert_thm (rwrls,anet)
@@ -558,12 +558,12 @@
let val tsig = #tsig(Sign.rep_sg sg);
val k = length aTs;
fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
- let val ca = Sign.cterm_of sg va
- and cx = Sign.cterm_of sg (eta_Var(("X"^si,0),T))
- val cb = Sign.cterm_of sg vb
- and cy = Sign.cterm_of sg (eta_Var(("Y"^si,0),T))
- val cP = Sign.cterm_of sg P
- and cp = Sign.cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
+ let val ca = cterm_of sg va
+ and cx = cterm_of sg (eta_Var(("X"^si,0),T))
+ val cb = cterm_of sg vb
+ and cy = cterm_of sg (eta_Var(("Y"^si,0),T))
+ val cP = cterm_of sg P
+ and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;
fun mk(c,T::Ts,i,yik) =
let val si = radixstring(26,"a",i)
--- a/src/LCF/fix.ML Tue Jan 18 15:57:40 1994 +0100
+++ b/src/LCF/fix.ML Tue Jan 18 16:37:12 1994 +0100
@@ -64,7 +64,7 @@
when submitted as an argument to SIMP_THM *)
(*
local
-val thm = trivial(Sign.read_cterm(sign_of LCF.thy)
+val thm = trivial(read_cterm(sign_of LCF.thy)
("<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)",propT));
val tac = EVERY1[rtac lfp_is_FIX, simp_tac ss,
strip_tac, simp_tac (LCF_ss addsimps [PROD_less]),
--- a/src/Provers/hypsubst.ML Tue Jan 18 15:57:40 1994 +0100
+++ b/src/Provers/hypsubst.ML Tue Jan 18 16:37:12 1994 +0100
@@ -79,7 +79,7 @@
val params = Logic.strip_params Bi
val var = liftvar (maxidx+1) (map #2 params)
and u = Unify.rlist_abs(rev params, t)
- and cterm = Sign.cterm_of sign
+ and cterm = cterm_of sign
in cterm_instantiate [(cterm var, cterm u)] (lift_rule (state,i) rule)
end;
--- a/src/Provers/simp.ML Tue Jan 18 15:57:40 1994 +0100
+++ b/src/Provers/simp.ML Tue Jan 18 16:37:12 1994 +0100
@@ -457,7 +457,7 @@
are represented by rules, generalized over their parameters*)
fun add_asms(ss,thm,a,anet,ats,cs) =
let val As = strip_varify(nth_subgoal i thm, a, []);
- val thms = map (trivial o Sign.cterm_of(#sign(rep_thm(thm))))As;
+ val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
val new_rws = flat(map mk_rew_rules thms);
val rwrls = map mk_trans (flat(map mk_rew_rules thms));
val anet' = foldr lhs_insert_thm (rwrls,anet)
@@ -585,12 +585,12 @@
let val tsig = #tsig(Sign.rep_sg sg);
val k = length aTs;
fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
- let val ca = Sign.cterm_of sg va
- and cx = Sign.cterm_of sg (eta_Var(("X"^si,0),T))
- val cb = Sign.cterm_of sg vb
- and cy = Sign.cterm_of sg (eta_Var(("Y"^si,0),T))
- val cP = Sign.cterm_of sg P
- and cp = Sign.cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
+ let val ca = cterm_of sg va
+ and cx = cterm_of sg (eta_Var(("X"^si,0),T))
+ val cb = cterm_of sg vb
+ and cy = cterm_of sg (eta_Var(("Y"^si,0),T))
+ val cP = cterm_of sg P
+ and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;
fun mk(c,T::Ts,i,yik) =
let val si = radixstring(26,"a",i)
--- a/src/Provers/splitter.ML Tue Jan 18 15:57:40 1994 +0100
+++ b/src/Provers/splitter.ML Tue Jan 18 16:37:12 1994 +0100
@@ -62,11 +62,11 @@
val Ts = map #2 (Logic.strip_params goali)
val _ $ t $ _ = Logic.strip_assums_concl goali;
val cntxt = mk_context cmap (rev Ts) (#maxidx(rep_thm lift)) t
- val cu = Sign.cterm_of sg cntxt
- val uT = #T(Sign.rep_cterm cu)
- val cP' = Sign.cterm_of sg (Var(P,uT))
+ val cu = cterm_of sg cntxt
+ val uT = #T(rep_cterm cu)
+ val cP' = cterm_of sg (Var(P,uT))
val ixnTs = Type.typ_match tsig ([],(PT,uT));
- val ixncTs = map (fn (x,y) => (x,Sign.ctyp_of sg y)) ixnTs;
+ val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs;
in instantiate (ixncTs, [(cP',cu)]) lift end;
fun splittable al i thm =
--- a/src/ZF/constructor.ML Tue Jan 18 15:57:40 1994 +0100
+++ b/src/ZF/constructor.ML Tue Jan 18 16:37:12 1994 +0100
@@ -55,7 +55,7 @@
(** Extract basic information from arguments **)
val sign = sign_of thy;
-val rdty = Sign.typ_of o Sign.read_ctyp sign;
+val rdty = typ_of o read_ctyp sign;
val rec_names = map #1 rec_specs;
--- a/src/ZF/ind_syntax.ML Tue Jan 18 15:57:40 1994 +0100
+++ b/src/ZF/ind_syntax.ML Tue Jan 18 16:37:12 1994 +0100
@@ -93,15 +93,15 @@
(*Prove a goal stated as a term, with exception handling*)
fun prove_term sign defs (P,tacsf) =
- let val ct = Sign.cterm_of sign P
+ let val ct = cterm_of sign P
in prove_goalw_cterm defs ct tacsf
handle e => (writeln ("Exception in proof of\n" ^
- Sign.string_of_cterm ct);
+ string_of_cterm ct);
raise e)
end;
(*Read an assumption in the given theory*)
-fun assume_read thy a = assume (Sign.read_cterm (sign_of thy) (a,propT));
+fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
(*Make distinct individual variables a1, a2, a3, ..., an. *)
fun mk_frees a [] = []
--- a/src/ZF/intr_elim.ML Tue Jan 18 15:57:40 1994 +0100
+++ b/src/ZF/intr_elim.ML Tue Jan 18 16:37:12 1994 +0100
@@ -104,11 +104,11 @@
val sign = sign_of Ind.thy;
fun rd T a =
- Sign.read_cterm sign (a,T)
+ read_cterm sign (a,T)
handle ERROR => error ("The error above occurred for " ^ a);
val rec_names = map #1 rec_doms
-and domts = map (Sign.term_of o rd iT o #2) rec_doms;
+and domts = map (term_of o rd iT o #2) rec_doms;
val dummy = assert_all Syntax.is_identifier rec_names
(fn a => "Name of recursive set not an identifier: " ^ a);
@@ -116,7 +116,7 @@
val dummy = assert_all (is_some o lookup_const sign) rec_names
(fn a => "Name of recursive set not declared as constant: " ^ a);
-val intr_tms = map (Sign.term_of o rd propT) sintrs;
+val intr_tms = map (term_of o rd propT) sintrs;
local (*Checking the introduction rules*)
val intr_sets = map (#2 o rule_concl) intr_tms;