--- a/QuotMain.thy	Fri Aug 28 10:01:25 2009 +0200
+++ b/QuotMain.thy	Fri Aug 28 17:12:19 2009 +0200
@@ -253,9 +253,9 @@
   var  "nat" 
 | app  "trm" "trm"
 | lam  "nat" "trm"
-  
-consts R :: "trm \<Rightarrow> trm \<Rightarrow> bool"
-axioms r_eq: "EQUIV R"
+
+axiomatization R :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
+  r_eq: "EQUIV R"
 
 ML {*
   typedef_main 
@@ -275,7 +275,7 @@
 thm Rep_qtrm
 
 text {* another test *}
-datatype 'a my = foo
+datatype 'a my = Foo
 consts Rmy :: "'a my \<Rightarrow> 'a my \<Rightarrow> bool"
 axioms rmy_eq: "EQUIV Rmy"
 
@@ -478,9 +478,9 @@
 term AP'
 
 text {* finite set example *}
-
+print_syntax
 inductive 
-  list_eq ("_ \<approx> _")
+  list_eq (infix "\<approx>" 50)
 where
   "a#b#xs \<approx> b#a#xs"
 | "[] \<approx> []"
@@ -491,15 +491,15 @@
 
 lemma list_eq_sym:
   shows "xs \<approx> xs"
-apply(induct xs)
-apply(auto intro: list_eq.intros)
-done
+  apply (induct xs)
+   apply (auto intro: list_eq.intros)
+  done
 
 lemma equiv_list_eq:
   shows "EQUIV list_eq"
-unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
-apply(auto intro: list_eq.intros list_eq_sym)
-done
+  unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
+  apply(auto intro: list_eq.intros list_eq_sym)
+  done
 
 local_setup {*
   typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
@@ -547,8 +547,8 @@
    for fset *) 
 
 ML {* val mthd = Method.SIMPLE_METHOD (rtac @{thm QUOT_TYPE_fset} 1 THEN
-  simp_tac (HOL_basic_ss addsimps @{thms REP_fset_def[symmetric]}) 1 THEN
-  simp_tac (HOL_basic_ss addsimps @{thms ABS_fset_def[symmetric]}) 1) *}
+  simp_tac (HOL_basic_ss addsimps @{thms REP_fset_def [symmetric]}) 1 THEN
+  simp_tac (HOL_basic_ss addsimps @{thms ABS_fset_def [symmetric]}) 1) *}
 ML {* val mthdt = Method.Basic (fn _ => mthd) *}
 ML {* val bymt = Proof.global_terminal_proof (mthdt, NONE) *}
 ML {* val exp_i = [((Locale.intern @{theory} "QUOT_TYPE"),(("QUOT_TYPE_fset_i", true),
@@ -577,8 +577,8 @@
 
 
 
-fun 
-  membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("_ memb _")
+fun
+  membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)
 where
   m1: "(x memb []) = False"
 | m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
@@ -587,30 +587,29 @@
   fixes z
   assumes a: "list_eq x y"
   shows "(z memb x) = (z memb y)"
-using a
-apply(induct)
-apply(auto)
-done
+  using a by induct auto
+
 
 lemma cons_preserves:
   fixes z
   assumes a: "xs \<approx> ys"
   shows "(z # xs) \<approx> (z # ys)"
-using a
-apply (rule QuotMain.list_eq.intros(5))
-done
+  using a by (rule QuotMain.list_eq.intros(5))
 
 ML {*
 fun unlam_def orig_ctxt ctxt t =
-  let
-    val (v, rest) = Thm.dest_abs NONE (Thm.rhs_of t)
-    val (vname, vt) = Term.dest_Free (Thm.term_of v)
-    val ([vnname], ctxt) = Variable.variant_fixes [vname] ctxt
-    val nv = Free(vnname, vt)
-    val t2 = Drule.fun_cong_rule t (Thm.cterm_of @{theory} nv)
-    val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2
-  in unlam_def orig_ctxt ctxt tnorm end
-  handle CTERM _ => singleton (ProofContext.export ctxt orig_ctxt) t
+  let val rhs = Thm.rhs_of t in
+  (case try (Thm.dest_abs NONE) rhs of
+    SOME (v, vt) =>
+      let
+        val (vname, vt) = Term.dest_Free (Thm.term_of v)
+        val ([vnname], ctxt) = Variable.variant_fixes [vname] ctxt
+        val nv = Free(vnname, vt)
+        val t2 = Drule.fun_cong_rule t (Thm.cterm_of (ProofContext.theory_of ctxt) nv)
+        val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2
+      in unlam_def orig_ctxt ctxt tnorm end
+  | NONE => singleton (ProofContext.export ctxt orig_ctxt) t)
+  end
 *}
 
 local_setup {*