# HG changeset patch
# User lcp
# Date 758907432 -3600
# Node ID cb6a244515444b22fb02f8bca1656c24fd0dfbf2
# Parent  ec8a2b6aa8a7ee30e00544a66c7c373b6506a05f
Updated refs to old Sign functions

diff -r ec8a2b6aa8a7 -r cb6a24451544 src/FOLP/simp.ML
--- 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)
diff -r ec8a2b6aa8a7 -r cb6a24451544 src/LCF/fix.ML
--- 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]),
diff -r ec8a2b6aa8a7 -r cb6a24451544 src/Provers/hypsubst.ML
--- 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;
 
diff -r ec8a2b6aa8a7 -r cb6a24451544 src/Provers/simp.ML
--- 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)
diff -r ec8a2b6aa8a7 -r cb6a24451544 src/Provers/splitter.ML
--- 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 =
diff -r ec8a2b6aa8a7 -r cb6a24451544 src/ZF/constructor.ML
--- 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;
 
diff -r ec8a2b6aa8a7 -r cb6a24451544 src/ZF/ind_syntax.ML
--- 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 [] = []
diff -r ec8a2b6aa8a7 -r cb6a24451544 src/ZF/intr_elim.ML
--- 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;