--- a/Quot/quotient_def.ML	Thu Jan 14 19:03:08 2010 +0100
+++ b/Quot/quotient_def.ML	Thu Jan 14 23:17:21 2010 +0100
@@ -24,24 +24,29 @@
 end
 
 
-(** interface and syntax setup **)
+(** Interface and Syntax Setup **)
 
-(* the ML-interface takes
+(* The ML-interface for a quotient definition takes 
+   as argument:
 
-  - the mixfix annotation
-  - name and attributes
-  - the new constant as term
-  - the rhs of the definition as term
+    - the mixfix annotation
+    - name and attributes
+    - the new constant as term
+    - the rhs of the definition as term
 
-  it returns the defined constant and its definition
-  theorem; stores the data in the qconsts slot       
+   It returns the defined constant and its definition
+   theorem; stores the data in the qconsts data slot. 
+
+   Restriction: At the moment the right-hand side must
+   be a terms composed of constant. Similarly the 
+   left-hand side must be a single constant.   
 *)
 fun quotient_def mx attr lhs rhs lthy =
 let
-  val (lhs_str, lhs_ty) =
-    dest_Free lhs
-    handle TERM _ => error "The name for the new constant has to be a Free; check that it is not defined yet."
-  val qconst_bname = Binding.name lhs_str;
+  val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
+  val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
+
+  val qconst_bname = Binding.name lhs_str
   val absrep_trm = absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs
   val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
   val (_, prop') = LocalDefs.cert_def lthy prop
@@ -62,6 +67,7 @@
 let
   val lhs = Syntax.read_term lthy lhs_str
   val rhs = Syntax.read_term lthy rhs_str
+  (* FIXME: Relating the reads will cause errors. *) 
 in
   quotient_def mx attr lhs rhs lthy |> snd
 end