--- a/QuotMain.thy	Tue Oct 06 11:56:23 2009 +0200
+++ b/QuotMain.thy	Tue Oct 06 15:11:30 2009 +0200
@@ -143,34 +143,34 @@
 section {* type definition for the quotient type *}
 
 ML {*
-(* constructs the term \<lambda>(c::ty \<Rightarrow> bool). \<exists>x. c = rel x *)
-fun typedef_term rel ty lthy =
+(* constructs the term \<lambda>(c::rty \<Rightarrow> bool). \<exists>x. c = rel x *)
+fun typedef_term rel rty lthy =
 let
-  val [x, c] = [("x", ty), ("c", ty --> @{typ bool})]
+  val [x, c] = [("x", rty), ("c", rty --> @{typ bool})]
                |> Variable.variant_frees lthy [rel]
                |> map Free
 in
   lambda c
-    (HOLogic.exists_const ty $
+    (HOLogic.exists_const rty $
        lambda x (HOLogic.mk_eq (c, (rel $ x))))
 end
 *}
 
 ML {*
 (* makes the new type definitions and proves non-emptyness*)
-fun typedef_make (qty_name, mx, rel, ty) lthy =
+fun typedef_make (qty_name, mx, rel, rty) lthy =
 let
   val typedef_tac =
      EVERY1 [rewrite_goal_tac @{thms mem_def},
              rtac @{thm exI},
              rtac @{thm exI},
              rtac @{thm refl}]
-  val tfrees = map fst (Term.add_tfreesT ty [])
+  val tfrees = map fst (Term.add_tfreesT rty [])
 in
   LocalTheory.theory_result
     (Typedef.add_typedef false NONE
        (qty_name, tfrees, mx)
-         (typedef_term rel ty lthy)
+         (typedef_term rel rty lthy)
            NONE typedef_tac) lthy
 end
 *}
@@ -202,13 +202,13 @@
   val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT)
   val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
              |> Syntax.check_term lthy
-  val _ = goal |> Syntax.string_of_term lthy |> tracing
 in
   Goal.prove lthy [] [] goal
     (K (typedef_quot_type_tac equiv_thm typedef_info))
 end
+*}
 
-
+ML {*
 (* proves the quotient theorem *)
 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
 let
@@ -255,10 +255,10 @@
 *}
 
 ML {*
-fun typedef_main (qty_name, mx, rel, ty, equiv_thm) lthy =
+fun typedef_main (qty_name, mx, rel, rty, equiv_thm) lthy =
 let
   (* generates typedef *)
-  val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, ty) lthy
+  val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy
 
   (* abs and rep functions *)
   val abs_ty = #abs_type typedef_info
@@ -440,7 +440,7 @@
   fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))
     | get_const repF = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty))
 
-  fun mk_identity ty = Abs ("x", ty, Bound 0)
+  fun mk_identity ty = Abs ("", ty, Bound 0)
 
 in
   if ty = qty
@@ -1048,26 +1048,26 @@
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 notation ( output) "Trueprop" ("#_" [1000] 1000)
 
-lemma atomize_eqv [atomize]: "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
-  (is "?rhs \<equiv> ?lhs")
+lemma atomize_eqv[atomize]: 
+  shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" 
 proof
-  assume "PROP ?lhs" then show "PROP ?rhs" by unfold
+  assume "A \<equiv> B" 
+  then show "Trueprop A \<equiv> Trueprop B" by unfold
 next
-  assume *: "PROP ?rhs"
+  assume *: "Trueprop A \<equiv> Trueprop B"
   have "A = B"
   proof (cases A)
     case True
-    with * have B by unfold
-    with `A` show ?thesis by simp
+    have "A" by fact
+    then show "A = B" using * by simp
   next
     case False
-    with * have "~ B" by auto
-    with `~ A` show ?thesis by simp
+    have "\<not>A" by fact
+    then show "A = B" using * by auto
   qed
-  then show "PROP ?lhs" by (rule eq_reflection)
+  then show "A \<equiv> B" by (rule eq_reflection)
 qed
 
-
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (atomize(full))