--- a/QuotMain.thy	Mon Sep 21 18:18:29 2009 +0200
+++ b/QuotMain.thy	Tue Sep 22 09:42:27 2009 +0200
@@ -347,12 +347,6 @@
 thm Rep_qtrm
 
 text {* another test *}
-datatype 'a my = Foo
-consts Rmy :: "'a my \<Rightarrow> 'a my \<Rightarrow> bool"
-axioms rmy_eq: "EQUIV Rmy"
-
-term "\<lambda>(c::'a my\<Rightarrow>bool). \<exists>x. c = Rmy x"
-
 datatype 'a trm' =
   var'  "'a"
 | app'  "'a trm'" "'a trm'"
@@ -409,11 +403,10 @@
 (* mapfuns for some standard types *)
 setup {*
     Context.theory_map (update @{type_name "list"} {mapfun = @{const_name "map"}})
- #> Context.theory_map (update @{type_name "*"} {mapfun = @{const_name "prod_fun"}})
+ #> Context.theory_map (update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}})
  #> Context.theory_map (update @{type_name "fun"}  {mapfun = @{const_name "fun_map"}})
 *}
 
-
 ML {* lookup (Context.Proof @{context}) @{type_name list} *}
 
 ML {*
@@ -616,6 +609,7 @@
 
 (* Maybe the infrastructure should not allow this kind of definition, without showing that
    the relation respects lenght... *)
+(* cu: what does this mean? *)
 local_setup {*
   make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
@@ -648,6 +642,7 @@
   shows "(z # xs) \<approx> (z # ys)"
   using a by (rule QuotMain.list_eq.intros(5))
 
+(* cu: what does unlam do? *)
 ML {*
 fun unlam_def orig_ctxt ctxt t =
   let val rhs = Thm.rhs_of t in