# HG changeset patch
# User kuncar
# Date 1323450424 -3600
# Node ID b16f976db51519b759ed5a4511998922ff574b70
# Parent  5616fbda86e6ed33d0b669816e24b0c386dc01c9
Quotient_Info stores only relation maps

diff -r 5616fbda86e6 -r b16f976db515 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Fri Dec 09 16:08:32 2011 +0100
+++ b/src/HOL/Library/Quotient_List.thy	Fri Dec 09 18:07:04 2011 +0100
@@ -8,7 +8,7 @@
 imports Main Quotient_Syntax
 begin
 
-declare [[map list = (map, list_all2)]]
+declare [[map list = list_all2]]
 
 lemma map_id [id_simps]:
   "map id = id"
diff -r 5616fbda86e6 -r b16f976db515 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Fri Dec 09 16:08:32 2011 +0100
+++ b/src/HOL/Library/Quotient_Option.thy	Fri Dec 09 18:07:04 2011 +0100
@@ -16,7 +16,7 @@
 | "option_rel R None (Some x) = False"
 | "option_rel R (Some x) (Some y) = R x y"
 
-declare [[map option = (Option.map, option_rel)]]
+declare [[map option = option_rel]]
 
 lemma option_rel_unfold:
   "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
diff -r 5616fbda86e6 -r b16f976db515 src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy	Fri Dec 09 16:08:32 2011 +0100
+++ b/src/HOL/Library/Quotient_Product.thy	Fri Dec 09 18:07:04 2011 +0100
@@ -13,7 +13,7 @@
 where
   "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
 
-declare [[map prod = (map_pair, prod_rel)]]
+declare [[map prod = prod_rel]]
 
 lemma prod_rel_apply [simp]:
   "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
diff -r 5616fbda86e6 -r b16f976db515 src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Fri Dec 09 16:08:32 2011 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy	Fri Dec 09 18:07:04 2011 +0100
@@ -16,7 +16,7 @@
 | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
 | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
 
-declare [[map sum = (sum_map, sum_rel)]]
+declare [[map sum = sum_rel]]
 
 lemma sum_rel_unfold:
   "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
diff -r 5616fbda86e6 -r b16f976db515 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Fri Dec 09 16:08:32 2011 +0100
+++ b/src/HOL/Quotient.thy	Fri Dec 09 18:07:04 2011 +0100
@@ -671,8 +671,8 @@
 use "Tools/Quotient/quotient_info.ML"
 setup Quotient_Info.setup
 
-declare [[map "fun" = (map_fun, fun_rel)]]
-declare [[map set = (vimage, set_rel)]]
+declare [[map "fun" = fun_rel]]
+declare [[map set = set_rel]]
 
 lemmas [quot_thm] = fun_quotient
 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
diff -r 5616fbda86e6 -r b16f976db515 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Dec 09 16:08:32 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Dec 09 18:07:04 2011 +0100
@@ -6,7 +6,7 @@
 
 signature QUOTIENT_INFO =
 sig
-  type quotmaps = {mapfun: string, relmap: string}
+  type quotmaps = {relmap: string}
   val lookup_quotmaps: Proof.context -> string -> quotmaps option
   val lookup_quotmaps_global: theory -> string -> quotmaps option
   val print_quotmaps: Proof.context -> unit
@@ -54,7 +54,7 @@
 (* FIXME just one data slot (record) per program unit *)
 
 (* info about map- and rel-functions for a type *)
-type quotmaps = {mapfun: string, relmap: string}
+type quotmaps = {relmap: string}
 
 structure Quotmaps = Generic_Data
 (
@@ -72,20 +72,18 @@
 val quotmaps_attribute_setup =
   Attrib.setup @{binding map}
     ((Args.type_name false --| Scan.lift (Parse.$$$ "=")) --  (* FIXME Args.type_name true (requires "set" type) *)
-      (Scan.lift (Parse.$$$ "(") |-- Args.const_proper true --| Scan.lift (Parse.$$$ ",") --
-        Args.const_proper true --| Scan.lift (Parse.$$$ ")")) >>
-      (fn (tyname, (mapname, relname)) =>
-        let val minfo = {mapfun = mapname, relmap = relname}
+      Args.const_proper true >>
+      (fn (tyname, relname) =>
+        let val minfo = {relmap = relname}
         in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
     "declaration of map information"
 
 fun print_quotmaps ctxt =
   let
-    fun prt_map (ty_name, {mapfun, relmap}) =
+    fun prt_map (ty_name, {relmap}) =
       Pretty.block (separate (Pretty.brk 2)
         (map Pretty.str
          ["type:", ty_name,
-          "map:", mapfun,
           "relation map:", relmap]))
   in
     map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))