Updated refs to old Sign functions
authorlcp
Tue Jan 18 16:37:12 1994 +0100 (1994-01-18)
changeset 231cb6a24451544
parent 230 ec8a2b6aa8a7
child 232 c28d2fc5dd1c
Updated refs to old Sign functions
src/FOLP/simp.ML
src/LCF/fix.ML
src/Provers/hypsubst.ML
src/Provers/simp.ML
src/Provers/splitter.ML
src/ZF/constructor.ML
src/ZF/ind_syntax.ML
src/ZF/intr_elim.ML
     1.1 --- a/src/FOLP/simp.ML	Tue Jan 18 15:57:40 1994 +0100
     1.2 +++ b/src/FOLP/simp.ML	Tue Jan 18 16:37:12 1994 +0100
     1.3 @@ -436,7 +436,7 @@
     1.4        are represented by rules, generalized over their parameters*)
     1.5  fun add_asms(ss,thm,a,anet,ats,cs) =
     1.6      let val As = strip_varify(nth_subgoal i thm, a, []);
     1.7 -	val thms = map (trivial o Sign.cterm_of(#sign(rep_thm(thm))))As;
     1.8 +	val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
     1.9  	val new_rws = flat(map mk_rew_rules thms);
    1.10  	val rwrls = map mk_trans (flat(map mk_rew_rules thms));
    1.11  	val anet' = foldr lhs_insert_thm (rwrls,anet)
    1.12 @@ -558,12 +558,12 @@
    1.13  let val tsig = #tsig(Sign.rep_sg sg);
    1.14      val k = length aTs;
    1.15      fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
    1.16 -	let val ca = Sign.cterm_of sg va
    1.17 -	    and cx = Sign.cterm_of sg (eta_Var(("X"^si,0),T))
    1.18 -	    val cb = Sign.cterm_of sg vb
    1.19 -	    and cy = Sign.cterm_of sg (eta_Var(("Y"^si,0),T))
    1.20 -	    val cP = Sign.cterm_of sg P
    1.21 -	    and cp = Sign.cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
    1.22 +	let val ca = cterm_of sg va
    1.23 +	    and cx = cterm_of sg (eta_Var(("X"^si,0),T))
    1.24 +	    val cb = cterm_of sg vb
    1.25 +	    and cy = cterm_of sg (eta_Var(("Y"^si,0),T))
    1.26 +	    val cP = cterm_of sg P
    1.27 +	    and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
    1.28  	in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;
    1.29      fun mk(c,T::Ts,i,yik) =
    1.30  	let val si = radixstring(26,"a",i)
     2.1 --- a/src/LCF/fix.ML	Tue Jan 18 15:57:40 1994 +0100
     2.2 +++ b/src/LCF/fix.ML	Tue Jan 18 16:37:12 1994 +0100
     2.3 @@ -64,7 +64,7 @@
     2.4     when submitted as an argument to SIMP_THM *)
     2.5  (*
     2.6  local
     2.7 -val thm = trivial(Sign.read_cterm(sign_of LCF.thy)
     2.8 +val thm = trivial(read_cterm(sign_of LCF.thy)
     2.9          ("<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)",propT));
    2.10  val tac = EVERY1[rtac lfp_is_FIX, simp_tac ss,
    2.11  	  strip_tac, simp_tac (LCF_ss addsimps [PROD_less]),
     3.1 --- a/src/Provers/hypsubst.ML	Tue Jan 18 15:57:40 1994 +0100
     3.2 +++ b/src/Provers/hypsubst.ML	Tue Jan 18 16:37:12 1994 +0100
     3.3 @@ -79,7 +79,7 @@
     3.4        val params = Logic.strip_params Bi
     3.5        val var = liftvar (maxidx+1) (map #2 params)
     3.6        and u   = Unify.rlist_abs(rev params, t)
     3.7 -      and cterm = Sign.cterm_of sign
     3.8 +      and cterm = cterm_of sign
     3.9    in cterm_instantiate [(cterm var, cterm u)] (lift_rule (state,i) rule)
    3.10    end;
    3.11  
     4.1 --- a/src/Provers/simp.ML	Tue Jan 18 15:57:40 1994 +0100
     4.2 +++ b/src/Provers/simp.ML	Tue Jan 18 16:37:12 1994 +0100
     4.3 @@ -457,7 +457,7 @@
     4.4        are represented by rules, generalized over their parameters*)
     4.5  fun add_asms(ss,thm,a,anet,ats,cs) =
     4.6      let val As = strip_varify(nth_subgoal i thm, a, []);
     4.7 -	val thms = map (trivial o Sign.cterm_of(#sign(rep_thm(thm))))As;
     4.8 +	val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
     4.9  	val new_rws = flat(map mk_rew_rules thms);
    4.10  	val rwrls = map mk_trans (flat(map mk_rew_rules thms));
    4.11  	val anet' = foldr lhs_insert_thm (rwrls,anet)
    4.12 @@ -585,12 +585,12 @@
    4.13  let val tsig = #tsig(Sign.rep_sg sg);
    4.14      val k = length aTs;
    4.15      fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
    4.16 -	let val ca = Sign.cterm_of sg va
    4.17 -	    and cx = Sign.cterm_of sg (eta_Var(("X"^si,0),T))
    4.18 -	    val cb = Sign.cterm_of sg vb
    4.19 -	    and cy = Sign.cterm_of sg (eta_Var(("Y"^si,0),T))
    4.20 -	    val cP = Sign.cterm_of sg P
    4.21 -	    and cp = Sign.cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
    4.22 +	let val ca = cterm_of sg va
    4.23 +	    and cx = cterm_of sg (eta_Var(("X"^si,0),T))
    4.24 +	    val cb = cterm_of sg vb
    4.25 +	    and cy = cterm_of sg (eta_Var(("Y"^si,0),T))
    4.26 +	    val cP = cterm_of sg P
    4.27 +	    and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
    4.28  	in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;
    4.29      fun mk(c,T::Ts,i,yik) =
    4.30  	let val si = radixstring(26,"a",i)
     5.1 --- a/src/Provers/splitter.ML	Tue Jan 18 15:57:40 1994 +0100
     5.2 +++ b/src/Provers/splitter.ML	Tue Jan 18 16:37:12 1994 +0100
     5.3 @@ -62,11 +62,11 @@
     5.4        val Ts = map #2 (Logic.strip_params goali)
     5.5        val _ $ t $ _ = Logic.strip_assums_concl goali;
     5.6        val cntxt = mk_context cmap (rev Ts) (#maxidx(rep_thm lift)) t
     5.7 -      val cu = Sign.cterm_of sg cntxt
     5.8 -      val uT = #T(Sign.rep_cterm cu)
     5.9 -      val cP' = Sign.cterm_of sg (Var(P,uT))
    5.10 +      val cu = cterm_of sg cntxt
    5.11 +      val uT = #T(rep_cterm cu)
    5.12 +      val cP' = cterm_of sg (Var(P,uT))
    5.13        val ixnTs = Type.typ_match tsig ([],(PT,uT));
    5.14 -      val ixncTs = map (fn (x,y) => (x,Sign.ctyp_of sg y)) ixnTs;
    5.15 +      val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs;
    5.16    in instantiate (ixncTs, [(cP',cu)]) lift end;
    5.17  
    5.18  fun splittable al i thm =
     6.1 --- a/src/ZF/constructor.ML	Tue Jan 18 15:57:40 1994 +0100
     6.2 +++ b/src/ZF/constructor.ML	Tue Jan 18 16:37:12 1994 +0100
     6.3 @@ -55,7 +55,7 @@
     6.4  (** Extract basic information from arguments **)
     6.5  
     6.6  val sign = sign_of thy;
     6.7 -val rdty = Sign.typ_of o Sign.read_ctyp sign;
     6.8 +val rdty = typ_of o read_ctyp sign;
     6.9  
    6.10  val rec_names = map #1 rec_specs;
    6.11  
     7.1 --- a/src/ZF/ind_syntax.ML	Tue Jan 18 15:57:40 1994 +0100
     7.2 +++ b/src/ZF/ind_syntax.ML	Tue Jan 18 16:37:12 1994 +0100
     7.3 @@ -93,15 +93,15 @@
     7.4  
     7.5  (*Prove a goal stated as a term, with exception handling*)
     7.6  fun prove_term sign defs (P,tacsf) = 
     7.7 -    let val ct = Sign.cterm_of sign P
     7.8 +    let val ct = cterm_of sign P
     7.9      in  prove_goalw_cterm defs ct tacsf
    7.10  	handle e => (writeln ("Exception in proof of\n" ^
    7.11 -			       Sign.string_of_cterm ct); 
    7.12 +			       string_of_cterm ct); 
    7.13  		     raise e)
    7.14      end;
    7.15  
    7.16  (*Read an assumption in the given theory*)
    7.17 -fun assume_read thy a = assume (Sign.read_cterm (sign_of thy) (a,propT));
    7.18 +fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
    7.19  
    7.20  (*Make distinct individual variables a1, a2, a3, ..., an. *)
    7.21  fun mk_frees a [] = []
     8.1 --- a/src/ZF/intr_elim.ML	Tue Jan 18 15:57:40 1994 +0100
     8.2 +++ b/src/ZF/intr_elim.ML	Tue Jan 18 16:37:12 1994 +0100
     8.3 @@ -104,11 +104,11 @@
     8.4  val sign = sign_of Ind.thy;
     8.5  
     8.6  fun rd T a = 
     8.7 -    Sign.read_cterm sign (a,T)
     8.8 +    read_cterm sign (a,T)
     8.9      handle ERROR => error ("The error above occurred for " ^ a);
    8.10  
    8.11  val rec_names = map #1 rec_doms
    8.12 -and domts     = map (Sign.term_of o rd iT o #2) rec_doms;
    8.13 +and domts     = map (term_of o rd iT o #2) rec_doms;
    8.14  
    8.15  val dummy = assert_all Syntax.is_identifier rec_names
    8.16     (fn a => "Name of recursive set not an identifier: " ^ a);
    8.17 @@ -116,7 +116,7 @@
    8.18  val dummy = assert_all (is_some o lookup_const sign) rec_names
    8.19     (fn a => "Name of recursive set not declared as constant: " ^ a);
    8.20  
    8.21 -val intr_tms = map (Sign.term_of o rd propT) sintrs;
    8.22 +val intr_tms = map (term_of o rd propT) sintrs;
    8.23  
    8.24  local (*Checking the introduction rules*)
    8.25    val intr_sets = map (#2 o rule_concl) intr_tms;