Type.typ_instance;
authorwenzelm
Fri May 21 21:18:14 2004 +0200 (2004-05-21)
changeset 14772c52060b69a8c
parent 14771 c2bf21b5564e
child 14773 556d9cc73711
Type.typ_instance;
src/FOLP/simp.ML
src/Provers/ind.ML
src/Provers/simp.ML
     1.1 --- a/src/FOLP/simp.ML	Fri May 21 21:17:37 2004 +0200
     1.2 +++ b/src/FOLP/simp.ML	Fri May 21 21:18:14 2004 +0200
     1.3 @@ -549,7 +549,7 @@
     1.4          let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
     1.5              val [P] = add_term_vars(concl_of thm,[]) \\ [va,vb]
     1.6              val eqT::_ = binder_types cT
     1.7 -        in if Type.typ_instance(tsig,T,eqT) then Some(thm,va,vb,P)
     1.8 +        in if Type.typ_instance tsig (T,eqT) then Some(thm,va,vb,P)
     1.9             else find thms
    1.10          end
    1.11        | find [] = None
    1.12 @@ -581,7 +581,7 @@
    1.13      val tsig = Sign.tsig_of sg;
    1.14      fun find_refl(r::rs) =
    1.15          let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
    1.16 -        in if Type.typ_instance(tsig, rT, hd(binder_types eqT))
    1.17 +        in if Type.typ_instance tsig (rT, hd(binder_types eqT))
    1.18             then Some(r,(eq,body_type eqT)) else find_refl rs
    1.19          end
    1.20        | find_refl([]) = None;
     2.1 --- a/src/Provers/ind.ML	Fri May 21 21:17:37 2004 +0200
     2.2 +++ b/src/Provers/ind.ML	Fri May 21 21:18:14 2004 +0200
     2.3 @@ -29,7 +29,7 @@
     2.4  
     2.5  fun add_term_frees tsig =
     2.6  let fun add(tm, vars) = case tm of
     2.7 -	Free(v,T) => if Type.typ_instance(tsig,T,aT) then v ins vars
     2.8 +	Free(v,T) => if Type.typ_instance tsig (T,aT) then v ins vars
     2.9  		     else vars
    2.10        | Abs (_,_,body) => add(body,vars)
    2.11        | rator$rand => add(rator, add(rand, vars))
     3.1 --- a/src/Provers/simp.ML	Fri May 21 21:17:37 2004 +0200
     3.2 +++ b/src/Provers/simp.ML	Fri May 21 21:18:14 2004 +0200
     3.3 @@ -575,7 +575,7 @@
     3.4  	let val (Const(_,cT), va, vb) =	dest_red(hd(prems_of thm));
     3.5  	    val [P] = term_vars(concl_of thm) \\ [va,vb]
     3.6  	    val eqT::_ = binder_types cT
     3.7 -        in if Type.typ_instance(tsig,T,eqT) then Some(thm,va,vb,P)
     3.8 +        in if Type.typ_instance tsig (T,eqT) then Some(thm,va,vb,P)
     3.9  	   else find thms
    3.10  	end
    3.11        | find [] = None
    3.12 @@ -607,7 +607,7 @@
    3.13      val tsig = Sign.tsig_of sg;
    3.14      fun find_refl(r::rs) =
    3.15  	let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
    3.16 -	in if Type.typ_instance(tsig, rT, hd(binder_types eqT))
    3.17 +	in if Type.typ_instance tsig (rT, hd(binder_types eqT))
    3.18  	   then Some(r,(eq,body_type eqT)) else find_refl rs
    3.19  	end
    3.20        | find_refl([]) = None;