Now deals with simples cases where the input equations contain type variables
See example in ReflectionEx.thy

--- a/src/HOL/ex/Reflection.thy	Fri Jan 26 13:59:06 2007 +0100
+++ b/src/HOL/ex/Reflection.thy	Sun Jan 28 11:52:52 2007 +0100
@@ -7,11 +7,12 @@
 
 theory Reflection
 imports Main
-uses ("reflection.ML")
+  uses ("reflection.ML")
 begin
 
 lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
   by (blast intro: ext)
+
 use "reflection.ML"
 
 method_setup reify = {*

--- a/src/HOL/ex/ReflectionEx.thy	Fri Jan 26 13:59:06 2007 +0100
+++ b/src/HOL/ex/ReflectionEx.thy	Sun Jan 28 11:52:52 2007 +0100
@@ -355,4 +355,38 @@
   apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
 oops
 
+
+  (* An example for equations containing type variables *)	
+datatype prod = Zero | One | Var nat | Mul prod prod 
+  | Pw prod nat | PNM nat nat prod
+consts Iprod :: "('a::{ordered_idom,recpower}) list \<Rightarrow> prod \<Rightarrow> 'a" 
+primrec
+  "Iprod vs Zero = 0"
+  "Iprod vs One = 1"
+  "Iprod vs (Var n) = vs!n"
+  "Iprod vs (Mul a b) = (Iprod vs a * Iprod vs b)"
+  "Iprod vs (Pw a n) = ((Iprod vs a) ^ n)"
+  "Iprod vs (PNM n k t) = (vs ! n)^k * Iprod vs t"
+consts prodmul:: "prod \<times> prod \<Rightarrow> prod"
+datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
+  | Or sgn sgn | And sgn sgn
+
+consts Isgn :: "('a::{ordered_idom, recpower}) list \<Rightarrow> sgn \<Rightarrow> bool"
+primrec 
+  "Isgn vs Tr = True"
+  "Isgn vs F = False"
+  "Isgn vs (ZeroEq t) = (Iprod vs t = 0)"
+  "Isgn vs (NZeroEq t) = (Iprod vs t \<noteq> 0)"
+  "Isgn vs (Pos t) = (Iprod vs t > 0)"
+  "Isgn vs (Neg t) = (Iprod vs t < 0)"
+  "Isgn vs (And p q) = (Isgn vs p \<and> Isgn vs q)"
+  "Isgn vs (Or p q) = (Isgn vs p \<or> Isgn vs q)"
+
+lemmas eqs = Isgn.simps Iprod.simps
+
+lemma "(x::int)^4 * y * z * y^2 * z^23 > 0"
+  apply (reify eqs)
+  oops
+
+
 end

--- a/src/HOL/ex/reflection.ML	Fri Jan 26 13:59:06 2007 +0100
+++ b/src/HOL/ex/reflection.ML	Sun Jan 28 11:52:52 2007 +0100
@@ -38,7 +38,7 @@
    val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt
    val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
    fun add_fterms (t as t1 $ t2) = 
-       if exists (fn f => (t |> strip_comb |> fst) aconv f) fs then insert (op aconv) t
+       if exists (fn f => could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
        else add_fterms t1 #> add_fterms t2
      | add_fterms (t as Abs(xn,xT,t')) = 
        if (fN mem (term_consts t)) then (fn _ => [t]) else (fn _ => [])
@@ -92,7 +92,7 @@
  let 
   val tt = HOLogic.listT (fastype_of t)
  in 
-  (case AList.lookup (op =) (!bds) tt of
+  (case AList.lookup Type.could_unify (!bds) tt of
     NONE => error "index_of : type not found in environements!"
   | SOME (tbs,tats) =>
     let
@@ -160,8 +160,8 @@
    in exists_Const 
 	  (fn (n,ty) => n="List.nth" 
 			andalso 
-			AList.defined (op =) (!bds) (domain_type ty)) rhs 
-	  andalso fastype_of rhs = tT
+			AList.defined Type.could_unify (!bds) (domain_type ty)) rhs 
+	  andalso Type.could_unify (fastype_of rhs, tT)
    end
   fun get_nth t = 
    case t of