# HG changeset patch
# User wenzelm
# Date 1085167094 -7200
# Node ID c52060b69a8cfcf9f0ffc0a75dfa274322712626
# Parent  c2bf21b5564e2f5cb3faca9474d85e49ccab0600
Type.typ_instance;

diff -r c2bf21b5564e -r c52060b69a8c src/FOLP/simp.ML
--- 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;
diff -r c2bf21b5564e -r c52060b69a8c src/Provers/ind.ML
--- 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))
diff -r c2bf21b5564e -r c52060b69a8c src/Provers/simp.ML
--- 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;