diff -r 8948319b190e -r 3e405c2fbe90 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Wed Feb 10 11:31:43 2010 +0100
+++ b/Quot/quotient_def.ML	Wed Feb 10 11:31:53 2010 +0100
@@ -73,9 +73,10 @@
 let
   val lhs = Syntax.read_term lthy lhs_str
   val rhs = Syntax.read_term lthy rhs_str
-  (* FIXME: Relating the reads will cause errors. *) 
+  val lthy' = Variable.declare_term lhs lthy
+  val lthy'' = Variable.declare_term rhs lthy'
 in
-  quotient_def mx attr lhs rhs lthy |> snd
+  quotient_def mx attr lhs rhs lthy'' |> snd
 end
 
 val _ = OuterKeyword.keyword "as";