diff -r c8187c293587 -r 72d63aa8af68 QuotMain.thy
--- a/QuotMain.thy	Fri Sep 25 19:26:18 2009 +0200
+++ b/QuotMain.thy	Mon Sep 28 02:39:44 2009 +0200
@@ -154,9 +154,8 @@
     (HOLogic.exists_const ty $ 
        lambda x (HOLogic.mk_eq (c, (rel $ x))))
 end
-*}
 
-ML {*
+
 (* makes the new type definitions and proves non-emptyness*)
 fun typedef_make (qty_name, rel, ty) lthy =
 let  
@@ -172,9 +171,8 @@
          (typedef_term rel ty lthy)
            NONE typedef_tac) lthy
 end
-*}
 
-ML {*
+
 (* tactic to prove the QUOT_TYPE theorem for the new type *)
 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
 let
@@ -195,6 +193,7 @@
           rtac rep_inj]
 end
 
+
 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
 let
   val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT)
@@ -204,9 +203,8 @@
   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
@@ -430,19 +428,22 @@
   in
    (case (lookup (Context.Proof lthy) s) of
       SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty))
-    | NONE => raise ERROR ("no map association for type " ^ s))
+    | NONE      => raise ERROR ("no map association for type " ^ s))
   end
 
   fun get_const abs = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))
     | get_const rep = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty))
+
+  fun mk_identity ty = Abs ("x", ty, Bound 0)
+
 in
   if ty = qty
   then (get_const abs_or_rep)
   else (case ty of
-          TFree _ => (Abs ("x", ty, Bound 0), (ty, ty))
-        | Type (_, []) => (Abs ("x", ty, Bound 0), (ty, ty))
+          TFree _ => (mk_identity ty, (ty, ty))
+        | Type (_, []) => (mk_identity ty, (ty, ty))
         | Type (s, tys) => get_fun_aux s (map (get_fun abs_or_rep rty qty lthy) tys)
-        | _ => raise ERROR ("no variables")
+        | _ => raise ERROR ("no type variables")
        )
 end
 *}
@@ -455,6 +456,7 @@
 *}
 
 
+text {* produces the definition for a lifted constant *}
 ML {*
 fun get_const_def nconst oconst rty qty lthy =
 let
@@ -478,11 +480,13 @@
 
 ML {*
 fun exchange_ty rty qty ty =
-  if ty = rty then qty
+  if ty = rty 
+  then qty
   else
     (case ty of
        Type (s, tys) => Type (s, map (exchange_ty rty qty) tys)
-      | _ => ty)
+      | _ => ty
+    )
 *}
 
 ML {*
@@ -498,20 +502,15 @@
 *}
 
 local_setup {*
-  make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd
-*}
-
-local_setup {*
-  make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd
-*}
-
-local_setup {*
+  make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
+  make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
   make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd
 *}
 
-thm VR_def
-thm AP_def
-thm LM_def
+term vr
+term ap
+term lm
+thm VR_def AP_def LM_def
 term LM
 term VR
 term AP
@@ -534,20 +533,15 @@
 print_theorems
 
 local_setup {*
-  make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
-*}
-
-local_setup {*
-  make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
-*}
-
-local_setup {*
+  make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
+  make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
   make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
 *}
 
-thm VR'_def
-thm AP'_def
-thm LM'_def
+term vr'
+term ap'
+term ap'
+thm VR'_def AP'_def LM'_def
 term LM'
 term VR'
 term AP'
@@ -648,7 +642,7 @@
  Maybe make_const_def should require a theorem that says that the particular lifted function
  respects the relation. With it such a definition would be impossible:
  make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*} *)
+*}*)
 
 lemma card1_rsp:
   fixes a b :: "'a list"
@@ -823,34 +817,39 @@
 
 ML {*
   fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
-  val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}, @{const_name "card1"}]
+  val consts = [@{const_name "Nil"}, @{const_name "append"}, 
+                @{const_name "Cons"}, @{const_name "membship"}, 
+                @{const_name "card1"}]
 *}
 
 ML {*
-fun build_goal thm constructors lifted_type mk_rep_abs =
-  let
+fun build_goal ctxt thm constructors qty mk_rep_abs =
+let
     fun is_const (Const (x, t)) = x mem constructors
       | is_const _ = false
+  
     fun maybe_mk_rep_abs t =
-      let
-        val _ = writeln ("Maybe: " ^ Syntax.string_of_term @{context} t)
-      in
-        if type_of t = lifted_type then mk_rep_abs t else t
-      end
-      handle TYPE _ => t
+    let
+      val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
+    in
+      if type_of t = qty then mk_rep_abs t else t
+    end
+    handle TYPE _ => t
+  
     fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr))
       | build_aux (f $ a) =
           let
             val (f, args) = strip_comb (f $ a)
-            val _ = writeln (Syntax.string_of_term @{context} f)
+            val _ = writeln (Syntax.string_of_term ctxt f)
            in
             (if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args))))
             else list_comb ((build_aux f), (map build_aux args)))
           end
       | build_aux x =
           if is_const x then maybe_mk_rep_abs x else x
+    
     val concl2 = term_of (#prop (crep_thm thm))
-  in
+in
   Logic.mk_equals ((build_aux concl2), concl2)
 end *}
 
@@ -942,7 +941,7 @@
 
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
-  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -958,7 +957,7 @@
 thm length_append (* Not true but worth checking that the goal is correct *)
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
-  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -970,7 +969,7 @@
 thm m2
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2}))
-  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -982,7 +981,7 @@
 thm list_eq.intros(4)
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)}))
-  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
   val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)
@@ -1024,7 +1023,7 @@
 thm list_eq.intros(5)
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)}))
-  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
 *}
 ML {*
   val cgoal = 
@@ -1049,7 +1048,7 @@
 ML {*
   val goal =
     Toplevel.program (fn () =>
-      build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+      build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
     )
 *}
 ML {*
@@ -1072,7 +1071,7 @@
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm card1_suc}))
 *}
 ML {*
-  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
 *}
 ML {*
   val cgoal = cterm_of @{theory} goal