--- a/QuotMain.thy	Mon Sep 21 10:53:01 2009 +0200
+++ b/QuotMain.thy	Mon Sep 21 18:18:01 2009 +0200
@@ -152,31 +152,26 @@
 end
 *}
 
-(*
 ML {*
- typedef_term @{term R} @{typ "nat"} @{context}
-  |> Syntax.string_of_term @{context}
-  |> writeln
-*}*)
-
-ML {*
-val typedef_tac =
-  EVERY1 [rewrite_goal_tac @{thms mem_def},
-          rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}]
+(* makes the new type definitions and proves non-emptyness*)
+fun typedef_make (qty_name, rel, ty) lthy =
+let  
+  val typedef_tac =
+     EVERY1 [rewrite_goal_tac @{thms mem_def},
+             rtac @{thm exI}, 
+             rtac @{thm exI}, 
+             rtac @{thm refl}]
+in
+  LocalTheory.theory_result
+    (Typedef.add_typedef false NONE
+       (qty_name, map fst (Term.add_tfreesT ty []), NoSyn)
+         (typedef_term rel ty lthy)
+           NONE typedef_tac) lthy
+end
 *}
 
 ML {*
-(* makes the new type definitions *)
-fun typedef_make (qty_name, rel, ty) lthy =
-  LocalTheory.theory_result
-  (Typedef.add_typedef false NONE
-     (qty_name, map fst (Term.add_tfreesT ty []), NoSyn)
-       (typedef_term rel ty lthy)
-         NONE typedef_tac) lthy
-*}
-
-text {* proves the QUOT_TYPE theorem for the new type *}
-ML {*
+(* proves the QUOT_TYPE theorem for the new type *)
 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
 let
   val rep_thm = #Rep typedef_info
@@ -195,14 +190,7 @@
           rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl},
           rtac rep_inj]
 end
-*}
 
-term QUOT_TYPE
-ML {* HOLogic.mk_Trueprop *}
-ML {* Goal.prove *}
-ML {* Syntax.check_term *}
-
-ML {*
 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
 let
   val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT)
@@ -210,26 +198,24 @@
              |> Syntax.check_term lthy
 in
   Goal.prove lthy [] [] goal
-    (fn _ => typedef_quot_type_tac equiv_thm typedef_info)
+    (K (typedef_quot_type_tac equiv_thm typedef_info))
 end
 *}
 
 ML {*
-fun typedef_quotient_thm_tac defs quot_type_thm =
-  EVERY1 [K (rewrite_goals_tac defs),
-          rtac @{thm QUOT_TYPE.QUOTIENT},
-          rtac quot_type_thm]
-*}
-
-ML {*
 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
 let
   val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT)
   val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
              |> Syntax.check_term lthy
+
+  val typedef_quotient_thm_tac =
+    EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]),
+            rtac @{thm QUOT_TYPE.QUOTIENT},
+            rtac quot_type_thm]
 in
-  Goal.prove lthy [] [] goal
-    (fn _ => typedef_quotient_thm_tac [abs_def, rep_def] quot_type_thm)
+  Goal.prove lthy [] [] goal 
+    (K typedef_quotient_thm_tac)
 end
 *}
 
@@ -245,7 +231,7 @@
 *}
 
 ML {*
-fun reg_thm (name, thm) lthy =
+fun note_thm (name, thm) lthy =
 let
   val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy
 in
@@ -265,7 +251,7 @@
 fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =
 let
   (* generates typedef *)
-  val ((_, typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy
+  val ((_, typedef_info), lthy1) = typedef_make (qty_name, rel, ty) lthy
 
   (* abs and rep functions *)
   val abs_ty = #abs_type typedef_info
@@ -278,30 +264,30 @@
   (* ABS and REP definitions *)
   val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )
   val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT )
-  val ABS_trm = Syntax.check_term lthy' (ABS_const $ rel $ abs)
-  val REP_trm = Syntax.check_term lthy' (REP_const $ rep)
+  val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs)
+  val REP_trm = Syntax.check_term lthy1 (REP_const $ rep)
   val ABS_name = Binding.prefix_name "ABS_" qty_name
   val REP_name = Binding.prefix_name "REP_" qty_name
-  val (((ABS, ABS_def), (REP, REP_def)), lthy'') =
-         lthy' |> make_def (ABS_name, NoSyn, ABS_trm)
+  val (((ABS, ABS_def), (REP, REP_def)), lthy2) =
+         lthy1 |> make_def (ABS_name, NoSyn, ABS_trm)
                ||>> make_def (REP_name, NoSyn, REP_trm)
 
   (* quot_type theorem *)
-  val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy''
+  val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2
   val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name
 
   (* quotient theorem *)
-  val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy''
+  val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
-  val ((_, [eqn1pre]), lthy''') = Variable.import true [ABS_def] lthy'';
+  val ((_, [eqn1pre]), lthy3) = Variable.import true [ABS_def] lthy2;
   val eqn1i = Thm.prop_of (symmetric eqn1pre)
-  val ((_, [eqn2pre]), lthy'''') = Variable.import true [REP_def] lthy''';
+  val ((_, [eqn2pre]), lthy4) = Variable.import true [REP_def] lthy3;
   val eqn2i = Thm.prop_of (symmetric eqn2pre)
 
-  val exp_morphism = ProofContext.export_morphism lthy'''' (ProofContext.init (ProofContext.theory_of lthy''''));
+  val exp_morphism = ProofContext.export_morphism lthy4 (ProofContext.init (ProofContext.theory_of lthy4));
   val exp_term = Morphism.term exp_morphism;
   val exp = Morphism.thm exp_morphism;
 
@@ -316,14 +302,14 @@
      ("Rep", rep)
     ]))]
 in
-  lthy''''
-  |> reg_thm (quot_thm_name, quot_thm)
-  ||>> reg_thm (quotient_thm_name, quotient_thm)
+  lthy4
+  |> note_thm (quot_thm_name, quot_thm)
+  ||>> note_thm (quotient_thm_name, quotient_thm)
   ||> LocalTheory.theory (fn thy =>
       let
         val global_eqns = map exp_term [eqn2i, eqn1i];
         (* Not sure if the following context should not be used *)
-        val (global_eqns2, lthy''''') = Variable.import_terms true global_eqns lthy'''';
+        val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4;
         val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
 end
@@ -335,13 +321,11 @@
 | app  "trm" "trm"
 | lam  "nat" "trm"
 
-axiomatization RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
+axiomatization 
+  RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" 
+where
   r_eq: "EQUIV RR"
 
-ML {*
-  typedef_main
-*}
-
 local_setup {*
   typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd
 *}
@@ -355,6 +339,7 @@
 
 (* Test interpretation *)
 thm QUOT_TYPE_I_qtrm.thm11
+thm QUOT_TYPE.thm11
 
 print_theorems