--- a/QuotMain.thy	Tue Oct 06 09:28:59 2009 +0200
+++ b/QuotMain.thy	Tue Oct 06 11:36:08 2009 +0200
@@ -744,7 +744,6 @@
 
   fun get_conv [] = Conv.rewr_conv def
     | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
- 
 in
   get_conv xs new_lhs |>  
   singleton (ProofContext.export ctxt' ctxt)
@@ -759,12 +758,9 @@
 term IN
 thm IN_def
 
-ML {* 
-  (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"}
-*}
-
+(* unlam_def tests *)
+ML {* (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"} *}
 ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*}
-
 ML {* @{thm IN_def}; unlam_def @{context} @{thm IN_def} *}
 
 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]
@@ -857,8 +853,6 @@
 ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *}
 ML {* val fall = Const(@{const_name all}, dummyT) *}
 
-ML {* Syntax.check_term *}
-
 ML {*
 fun build_goal_term ctxt thm constructors rty qty mk_rep mk_abs =
   let
@@ -923,6 +917,19 @@
   Logic.mk_equals ((build_goal_term ctxt thm cons rty qty mk_rep mk_abs), (Thm.prop_of thm))
 *}
 
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
+*}
+  
+ML {*
+m1_novars |> prop_of
+|> Syntax.string_of_term @{context}
+|> writeln; 
+build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
 
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
 ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *}