--- a/QuotMain.thy	Wed Nov 04 14:03:46 2009 +0100
+++ b/QuotMain.thy	Wed Nov 04 15:27:32 2009 +0100
@@ -372,12 +372,27 @@
   | _ => trm
 *}
 
+ML {*
+fun my_reg_inst lthy rel rty trm =
+  case rel of
+    Const (n, _) => Syntax.check_term lthy
+      (my_reg lthy (Const (n, dummyT)) rty trm)
+*}
+
+(*ML {*
+  (*val r = term_of @{cpat "R::?'a list \<Rightarrow> ?'a list \<Rightarrow>bool"};*)
+  val r = Free ("R", dummyT);
+  val t = (my_reg @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});
+  val t2 = Syntax.check_term @{context} t;
+  Toplevel.program (fn () => cterm_of @{theory} t2)
+*}*)
+
 text {* Assumes that the given theorem is atomized *}
 ML {*
   fun build_regularize_goal thm rty rel lthy =
      Logic.mk_implies
        ((prop_of thm),
-       (my_reg lthy rel rty (prop_of thm)))
+       (my_reg_inst lthy rel rty (prop_of thm)))
 *}
 
 lemma universal_twice: