src/FOLP/simp.ML
changeset 231 cb6a24451544
parent 0 a5a9c433f639
child 611 11098f505bfe
     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)