# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265738888 -3600
# Node ID 1e5dee9e6ae2db2da5317a767f0d05a5d6f3f6f3
# Parent  86093c201bac31719672472bcd9da45abe7f8c05
proper declaration of types and terms during parsing (removes the varifyT when storing data)

diff -r 86093c201bac -r 1e5dee9e6ae2 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Tue Feb 09 17:26:28 2010 +0100
+++ b/Quot/quotient_typ.ML	Tue Feb 09 19:08:08 2010 +0100
@@ -163,10 +163,8 @@
   val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
 
   (* storing the quot-info *)
-  (* FIXME: VarifyT should not be used - at the moment it allows matching against the types. *)
   fun qinfo phi = transform_quotdata phi
-    {qtyp = Logic.varifyT Abs_ty, rtyp = Logic.varifyT rty,
-     equiv_rel = map_types Logic.varifyT rel, equiv_thm = equiv_thm}
+    {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
   val lthy4 = Local_Theory.declaration true
     (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3
 in
@@ -273,17 +271,26 @@
            
 fun quotient_type_cmd specs lthy = 
 let
-  fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) =
+  fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy =
   let
-    (*val rty = Syntax.read_typ lthy rty_str*)
-    
+    (* new parsing with proper declaration *)
     val rty = Syntax.read_typ lthy rty_str
-    val rel = Syntax.read_term lthy rel_str 
+    val lthy1 = Variable.declare_typ rty lthy
+    val pre_rel = Syntax.parse_term lthy1 rel_str
+    val pre_rel' = Syntax.type_constraint (rty --> rty --> @{typ bool}) pre_rel
+    val rel = Syntax.check_term lthy1 pre_rel'   
+    val lthy2 = Variable.declare_term rel lthy1
+   
+    (* old parsing *)
+    (* val rty = Syntax.read_typ lthy rty_str
+       val rel = Syntax.read_term lthy rel_str *) 
   in
-    ((vs, qty_name, mx), (rty, rel))
+    (((vs, qty_name, mx), (rty, rel)), lthy2)
   end
+
+  val (spec', lthy') = fold_map parse_spec specs lthy
 in
-  quotient_type (map parse_spec specs) lthy
+  quotient_type spec' lthy'
 end
 
 val quotspec_parser =