# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263507441 -3600
# Node ID e49c6b6f37f4c45a27f087824f24cd770c5151f9
# Parent  99e811fc1366ba956857eec9125ce8009ef7ae61
tuned quotient_def.ML and cleaned somewhat LamEx.thy

diff -r 99e811fc1366 -r e49c6b6f37f4 Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Thu Jan 14 19:03:08 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Thu Jan 14 23:17:21 2010 +0100
@@ -360,18 +360,11 @@
 qed
 
 
-lemma var_supp:
-  shows "supp (Var a) = ((supp a)::name set)"
-  apply(simp add: supp_def)
-  apply(simp add: pi_var2)
-  apply(simp add: var_inject)
-  done
-
 lemma var_fresh:
   fixes a::"name"
   shows "(a \<sharp> (Var b)) = (a \<sharp> b)"
   apply(simp add: fresh_def)
-  apply(simp add: var_supp)
+  apply(simp add: var_supp1)
   done
 
 end
diff -r 99e811fc1366 -r e49c6b6f37f4 Quot/quotient_def.ML
--- 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