--- a/QuotMain.thy	Tue Sep 15 11:31:35 2009 +0200
+++ b/QuotMain.thy	Wed Sep 16 11:50:41 2009 +0200
@@ -180,12 +180,12 @@
 
 text {* two wrappers for define and note *}
 ML {*
-fun make_def (name, mx, trm) lthy =
+fun make_def (name, mx, rhs) lthy =
 let
-  val ((trm, (_ , thm)), lthy') =
-     LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, trm)) lthy
+  val ((rhs, (_ , thm)), lthy') =
+     LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy
 in
-  ((trm, thm), lthy')
+  ((rhs, thm), lthy')
 end
 *}
 
@@ -446,27 +446,27 @@
 *}
 
 ML {*
-fun make_const_def nconst_name oconst mx rty qty lthy =
+fun make_const_def nconst_bname oconst mx rty qty lthy =
 let
   val oconst_ty = fastype_of oconst
   val nconst_ty = exchange_ty rty qty oconst_ty
-  val nconst = Const (nconst_name, nconst_ty)
+  val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
   val def_trm = get_const_def nconst oconst rty qty lthy
 in
-  make_def (Binding.name nconst_name, mx, def_trm) lthy
+  make_def (nconst_bname, mx, def_trm) lthy
 end
 *}
 
 local_setup {*
-  make_const_def "VR" @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd
+  make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd
 *}
 
 local_setup {*
-  make_const_def "AP" @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd
+  make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd
 *}
 
 local_setup {*
-  make_const_def "LM" @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd
+  make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd
 *}
 
 thm VR_def
@@ -494,15 +494,15 @@
 print_theorems
 
 local_setup {*
-  make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
+  make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
 *}
 
 local_setup {*
-  make_const_def "AP'" @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
+  make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
 *}
 
 local_setup {*
-  make_const_def "LM'" @{term "lm'"} 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
@@ -547,7 +547,7 @@
 thm "Rep_fset"
 
 local_setup {*
-  make_const_def "EMPTY" @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term Nil
@@ -556,7 +556,7 @@
 
 
 local_setup {*
-  make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term Cons
@@ -564,7 +564,7 @@
 thm INSERT_def
 
 local_setup {*
-  make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term append
@@ -572,7 +572,7 @@
 thm UNION_def
 
 local_setup {*
-  make_const_def "CARD" @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term length
@@ -620,7 +620,7 @@
 *}
 
 local_setup {*
-  make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term membship