--- a/src/FOLP/simp.ML Fri May 21 21:17:37 2004 +0200
+++ b/src/FOLP/simp.ML Fri May 21 21:18:14 2004 +0200
@@ -549,7 +549,7 @@
let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
val [P] = add_term_vars(concl_of thm,[]) \\ [va,vb]
val eqT::_ = binder_types cT
- in if Type.typ_instance(tsig,T,eqT) then Some(thm,va,vb,P)
+ in if Type.typ_instance tsig (T,eqT) then Some(thm,va,vb,P)
else find thms
end
| find [] = None
@@ -581,7 +581,7 @@
val tsig = Sign.tsig_of sg;
fun find_refl(r::rs) =
let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
- in if Type.typ_instance(tsig, rT, hd(binder_types eqT))
+ in if Type.typ_instance tsig (rT, hd(binder_types eqT))
then Some(r,(eq,body_type eqT)) else find_refl rs
end
| find_refl([]) = None;
--- a/src/Provers/ind.ML Fri May 21 21:17:37 2004 +0200
+++ b/src/Provers/ind.ML Fri May 21 21:18:14 2004 +0200
@@ -29,7 +29,7 @@
fun add_term_frees tsig =
let fun add(tm, vars) = case tm of
- Free(v,T) => if Type.typ_instance(tsig,T,aT) then v ins vars
+ Free(v,T) => if Type.typ_instance tsig (T,aT) then v ins vars
else vars
| Abs (_,_,body) => add(body,vars)
| rator$rand => add(rator, add(rand, vars))
--- a/src/Provers/simp.ML Fri May 21 21:17:37 2004 +0200
+++ b/src/Provers/simp.ML Fri May 21 21:18:14 2004 +0200
@@ -575,7 +575,7 @@
let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
val [P] = term_vars(concl_of thm) \\ [va,vb]
val eqT::_ = binder_types cT
- in if Type.typ_instance(tsig,T,eqT) then Some(thm,va,vb,P)
+ in if Type.typ_instance tsig (T,eqT) then Some(thm,va,vb,P)
else find thms
end
| find [] = None
@@ -607,7 +607,7 @@
val tsig = Sign.tsig_of sg;
fun find_refl(r::rs) =
let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
- in if Type.typ_instance(tsig, rT, hd(binder_types eqT))
+ in if Type.typ_instance tsig (rT, hd(binder_types eqT))
then Some(r,(eq,body_type eqT)) else find_refl rs
end
| find_refl([]) = None;