# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1254145058 -7200
# Node ID 1d08221f48c4ada3e90fc001a0ef95c236482755
# Parent  3767a6f3d9ee83378c37dcd5ed887233d3ba5dd5
Instnatiation with a schematic variable

diff -r 3767a6f3d9ee -r 1d08221f48c4 QuotMain.thy
--- a/QuotMain.thy	Fri Sep 25 14:50:35 2009 +0200
+++ b/QuotMain.thy	Mon Sep 28 15:37:38 2009 +0200
@@ -910,6 +910,7 @@
       (bop, (lhs, rhs))
     end
 *}
+
 ML {*
   fun dest_ceq t =
     let
@@ -1161,6 +1162,28 @@
   )
 *}
 
+thm leqi4_lift
+ML {*
+  val (nam, typ) = (hd (Term.add_vars (term_of (#prop (crep_thm @{thm leqi4_lift}))) []))
+  val (_, l) = dest_Type typ
+  val t = Type ("QuotMain.fset", l)
+  val v = Var (nam, t)
+  val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v)
+*}
+
+ML {*
+term_of (#prop (crep_thm @{thm sym}))
+*}
+
+ML {*
+  Toplevel.program (fn () =>
+    MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
+      Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift}
+    )
+  )
+*}
+
+
 
 
 
@@ -1178,10 +1201,10 @@
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
 ML {* @{term "\<exists>x. P x"} *}
+ML {*  Thm.bicompose *}
 prove {* (Thm.term_of cgoal2) *}
-  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) 
   apply (tactic {* foo_tac' @{context} 1 *})
-  done
 
 
 (*