diff -r 00d141f2daa7 -r 0ffc37761e53 QuotMain.thy
--- a/QuotMain.thy	Wed Oct 21 14:09:06 2009 +0200
+++ b/QuotMain.thy	Wed Oct 21 14:15:22 2009 +0200
@@ -704,6 +704,7 @@
   trm == new_trm
 *)
 
+text {* Assumes that the given theorem is atomized *}
 ML {*
   fun build_regularize_goal thm rty rel lthy =
      Logic.mk_implies
@@ -713,7 +714,6 @@
 
 section {* RepAbs injection *}
 
-
 ML {*
 fun build_repabs_term lthy thm constructors rty qty =
   let
@@ -773,18 +773,15 @@
   end
 *}
 
+text {* Assumes that it is given a regularized theorem *}
 ML {*
 fun build_repabs_goal ctxt thm cons rty qty =
   Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
 *}
 
 
-
-
-
 section {* finite set example *}
 
-print_syntax
 inductive
   list_eq (infix "\<approx>" 50)
 where
@@ -1041,26 +1038,14 @@
   done
 
 ML {*
-  fun mk_rep x = @{term REP_fset} $ x;
-  fun mk_abs x = @{term ABS_fset} $ x;
   val consts = [@{const_name "Nil"}, @{const_name "Cons"},
                 @{const_name "membship"}, @{const_name "card1"},
                 @{const_name "append"}, @{const_name "fold1"}];
 *}
 
-ML {* val tm = @{term "x :: 'a list"} *}
-ML {* val ty = exchange_ty @{typ "'a list"} @{typ "'a fset"} (fastype_of tm) *}
-ML {* (fst (get_fun repF @{typ "'a list"} @{typ "'a fset"} @{context} ty)) $ tm *}
-
-ML {* val qty = @{typ "'a fset"} *}
-ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *}
-ML {* val fall = Const(@{const_name all}, dummyT) *}
-
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
 
-
-
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
 *}