diff -r 32c0985563a8 -r 6584b1ceedce QuotMain.thy
--- a/QuotMain.thy	Tue Sep 29 10:49:31 2009 +0200
+++ b/QuotMain.thy	Tue Sep 29 11:55:37 2009 +0200
@@ -857,7 +857,7 @@
         | _ =>
             if is_constructor head then
               maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args'))
-            else list_comb (head, args'))
+            else maybe_mk_rep_abs (list_comb (head, args')))
       end;
 
     val concl2 = Thm.prop_of thm;
@@ -1040,13 +1040,7 @@
 *}
 
 (* It is the same, but we need a name for it. *)
-prove {* Thm.term_of cgoal3 *}
-  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (tactic {* foo_tac' @{context} 1 *})
-  done
-lemma zzz :
-  "Trueprop (REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))
-    \<equiv> Trueprop (a # a # xs \<approx> a # xs)"
+prove zzz : {* Thm.term_of cgoal3 *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
   done
@@ -1139,20 +1133,6 @@
 thm leqi5_lift
 thm m2_lift
 thm card_suc
-(* The above is not good, we lost the ABS in front of xs on the rhs, so can't be properly instantiated... *)
-
-ML Drule.instantiate'
-text {*
-  We lost the schematic variable again :(.
-  Another variable export will still be necessary...
-*}
-ML {*
-  Toplevel.program (fn () =>
-    MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
-      Drule.instantiate' [] [NONE, NONE, SOME (@{cpat "REP_fset x"})] @{thm m2_lift}
-    )
-  )
-*}
 
 thm leqi4_lift
 ML {*
@@ -1164,10 +1144,6 @@
 *}
 
 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}
@@ -1175,7 +1151,27 @@
   )
 *}
 
-ML {* MRS *}
+thm card_suc
+ML {*
+  val (nam, typ) = (hd (tl (Term.add_vars (term_of (#prop (crep_thm @{thm card_suc}))) [])))
+  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 {*
+  Toplevel.program (fn () =>
+    MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
+      Drule.instantiate' [] [SOME (cv)] @{thm card_suc}
+    )
+  )
+*}
+
+
+
+
+
 thm card1_suc
 
 ML {*
@@ -1190,11 +1186,13 @@
 *}
 ML {* @{term "\<exists>x. P x"} *}
 ML {*  Thm.bicompose *}
-prove {* (Thm.term_of cgoal2) *}
+prove aaa: {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
   done
 
+thm aaa
+
 (*
 datatype obj1 =
   OVAR1 "string"