# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1257344852 -3600
# Node ID 5470176d67300792f4767a245ffc858af8d7e182
# Parent  e9212a4a44be0f4e2808667df05769cc8e14a7b8
Type instantiation in regularize

diff -r e9212a4a44be -r 5470176d6730 QuotMain.thy
--- 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: