use only one data slot; rename print_quotmaps to print_quot_maps; tuned
authorkuncar
Wed Aug 28 14:37:35 2013 +0200 (2013-08-28)
changeset 53219ca237b9e4542
parent 53218 9ddc3bf9f5df
child 53220 daa550823c9f
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
etc/isar-keywords.el
src/Doc/IsarRef/HOL_Specific.thy
src/HOL/Lifting.thy
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Lifting/lifting_term.ML
     1.1 --- a/etc/isar-keywords.el	Wed Aug 28 11:15:14 2013 +0200
     1.2 +++ b/etc/isar-keywords.el	Wed Aug 28 14:37:35 2013 +0200
     1.3 @@ -195,10 +195,10 @@
     1.4      "print_methods"
     1.5      "print_options"
     1.6      "print_orders"
     1.7 +    "print_quot_maps"
     1.8      "print_quotconsts"
     1.9      "print_quotients"
    1.10      "print_quotientsQ3"
    1.11 -    "print_quotmaps"
    1.12      "print_quotmapsQ3"
    1.13      "print_rules"
    1.14      "print_simpset"
    1.15 @@ -422,10 +422,10 @@
    1.16      "print_methods"
    1.17      "print_options"
    1.18      "print_orders"
    1.19 +    "print_quot_maps"
    1.20      "print_quotconsts"
    1.21      "print_quotients"
    1.22      "print_quotientsQ3"
    1.23 -    "print_quotmaps"
    1.24      "print_quotmapsQ3"
    1.25      "print_rules"
    1.26      "print_simpset"
     2.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Wed Aug 28 11:15:14 2013 +0200
     2.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Wed Aug 28 14:37:35 2013 +0200
     2.3 @@ -1550,7 +1550,7 @@
     2.4    \begin{matharray}{rcl}
     2.5      @{command_def (HOL) "setup_lifting"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
     2.6      @{command_def (HOL) "lift_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
     2.7 -    @{command_def (HOL) "print_quotmaps"} & : & @{text "context \<rightarrow>"}\\
     2.8 +    @{command_def (HOL) "print_quot_maps"} & : & @{text "context \<rightarrow>"}\\
     2.9      @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
    2.10      @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
    2.11      @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\
    2.12 @@ -1626,7 +1626,7 @@
    2.13      Integration with code: For total quotients, @{command
    2.14      (HOL) "lift_definition"} uses @{text f.abs_eq} as a code equation.
    2.15  
    2.16 -  \item @{command (HOL) "print_quotmaps"} prints stored quotient map
    2.17 +  \item @{command (HOL) "print_quot_maps"} prints stored quotient map
    2.18      theorems.
    2.19  
    2.20    \item @{command (HOL) "print_quotients"} prints stored quotient
     3.1 --- a/src/HOL/Lifting.thy	Wed Aug 28 11:15:14 2013 +0200
     3.2 +++ b/src/HOL/Lifting.thy	Wed Aug 28 14:37:35 2013 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4  imports Equiv_Relations Transfer
     3.5  keywords
     3.6    "parametric" and
     3.7 -  "print_quotmaps" "print_quotients" :: diag and
     3.8 +  "print_quot_maps" "print_quotients" :: diag and
     3.9    "lift_definition" :: thy_goal and
    3.10    "setup_lifting" :: thy_decl
    3.11  begin
     4.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Wed Aug 28 11:15:14 2013 +0200
     4.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Wed Aug 28 14:37:35 2013 +0200
     4.3 @@ -6,18 +6,15 @@
     4.4  
     4.5  signature LIFTING_INFO =
     4.6  sig
     4.7 -  type quotmaps = {rel_quot_thm: thm}
     4.8 -  val lookup_quotmaps: Proof.context -> string -> quotmaps option
     4.9 -  val lookup_quotmaps_global: theory -> string -> quotmaps option
    4.10 -  val print_quotmaps: Proof.context -> unit
    4.11 -
    4.12 -  type pcrel_info = {pcrel_def: thm, pcr_cr_eq: thm}
    4.13 -  type quotients = {quot_thm: thm, pcrel_info: pcrel_info option}
    4.14 -  val transform_quotients: morphism -> quotients -> quotients
    4.15 -  val lookup_quotients: Proof.context -> string -> quotients option
    4.16 -  val lookup_quotients_global: theory -> string -> quotients option
    4.17 -  val update_quotients: string -> quotients -> Context.generic -> Context.generic
    4.18 -  val dest_quotients: Proof.context -> quotients list
    4.19 +  type quot_map = {rel_quot_thm: thm}
    4.20 +  val lookup_quot_maps: Proof.context -> string -> quot_map option
    4.21 +  val print_quot_maps: Proof.context -> unit
    4.22 +  
    4.23 +  type pcr = {pcrel_def: thm, pcr_cr_eq: thm}
    4.24 +  type quotient = {quot_thm: thm, pcr_info: pcr option}
    4.25 +  val transform_quotient: morphism -> quotient -> quotient
    4.26 +  val lookup_quotients: Proof.context -> string -> quotient option
    4.27 +  val update_quotients: string -> quotient -> Context.generic -> Context.generic
    4.28    val print_quotients: Proof.context -> unit
    4.29  
    4.30    val get_invariant_commute_rules: Proof.context -> thm list
    4.31 @@ -29,7 +26,10 @@
    4.32    type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
    4.33      pos_distr_rules: thm list, neg_distr_rules: thm list}
    4.34    val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option
    4.35 -  val lookup_relator_distr_data_global: theory -> string -> relator_distr_data option
    4.36 +
    4.37 +  val get_quot_maps           : Proof.context -> quot_map Symtab.table
    4.38 +  val get_quotients           : Proof.context -> quotient Symtab.table
    4.39 +  val get_relator_distr_data  : Proof.context -> relator_distr_data Symtab.table
    4.40  
    4.41    val setup: theory -> theory
    4.42  end;
    4.43 @@ -39,23 +39,62 @@
    4.44  
    4.45  open Lifting_Util
    4.46  
    4.47 -(** data containers **)
    4.48 +(** data container **)
    4.49 +
    4.50 +type quot_map = {rel_quot_thm: thm}
    4.51 +type pcr = {pcrel_def: thm, pcr_cr_eq: thm}
    4.52 +type quotient = {quot_thm: thm, pcr_info: pcr option}
    4.53 +type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
    4.54 +  pos_distr_rules: thm list, neg_distr_rules: thm list}
    4.55 +
    4.56 +structure Data = Generic_Data
    4.57 +(
    4.58 +  type T = 
    4.59 +    { quot_maps : quot_map Symtab.table,
    4.60 +      quotients : quotient Symtab.table,
    4.61 +      reflexivity_rules : thm Item_Net.T,
    4.62 +      relator_distr_data : relator_distr_data Symtab.table
    4.63 +    }
    4.64 +  val empty =
    4.65 +    { quot_maps = Symtab.empty,
    4.66 +      quotients = Symtab.empty,
    4.67 +      reflexivity_rules = Thm.full_rules,
    4.68 +      relator_distr_data = Symtab.empty
    4.69 +    }
    4.70 +  val extend = I
    4.71 +  fun merge
    4.72 +    ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1 },
    4.73 +      { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2 } ) =
    4.74 +    { quot_maps = Symtab.merge (K true) (qm1, qm2),
    4.75 +      quotients = Symtab.merge (K true) (q1, q2),
    4.76 +      reflexivity_rules = Item_Net.merge (rr1, rr2),
    4.77 +      relator_distr_data = Symtab.merge (K true) (rdd1, rdd2) }
    4.78 +)
    4.79 +
    4.80 +fun map_data f1 f2 f3 f4
    4.81 +  { quot_maps, quotients, reflexivity_rules, relator_distr_data} =
    4.82 +  { quot_maps = f1 quot_maps,
    4.83 +    quotients = f2 quotients,
    4.84 +    reflexivity_rules = f3 reflexivity_rules,
    4.85 +    relator_distr_data = f4 relator_distr_data }
    4.86 +
    4.87 +fun map_quot_maps           f = map_data f I I I
    4.88 +fun map_quotients           f = map_data I f I I
    4.89 +fun map_reflexivity_rules   f = map_data I I f I
    4.90 +fun map_relator_distr_data  f = map_data I I I f
    4.91 +  
    4.92 +val get_quot_maps'           = #quot_maps o Data.get
    4.93 +val get_quotients'           = #quotients o Data.get
    4.94 +val get_reflexivity_rules'   = #reflexivity_rules o Data.get
    4.95 +val get_relator_distr_data'  = #relator_distr_data o Data.get
    4.96 +
    4.97 +fun get_quot_maps          ctxt = get_quot_maps' (Context.Proof ctxt)
    4.98 +fun get_quotients          ctxt = get_quotients' (Context.Proof ctxt)
    4.99 +fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt)
   4.100  
   4.101  (* info about Quotient map theorems *)
   4.102 -type quotmaps = {rel_quot_thm: thm}
   4.103  
   4.104 -structure Quotmaps = Generic_Data
   4.105 -(
   4.106 -  type T = quotmaps Symtab.table
   4.107 -  val empty = Symtab.empty
   4.108 -  val extend = I
   4.109 -  fun merge data = Symtab.merge (K true) data
   4.110 -)
   4.111 -
   4.112 -val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof
   4.113 -val lookup_quotmaps_global = Symtab.lookup o Quotmaps.get o Context.Theory
   4.114 -
   4.115 -(* FIXME export proper internal update operation!? *)
   4.116 +val lookup_quot_maps = Symtab.lookup o get_quot_maps
   4.117  
   4.118  fun quot_map_thm_sanity_check rel_quot_thm ctxt =
   4.119    let
   4.120 @@ -102,14 +141,14 @@
   4.121      val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs
   4.122      val minfo = {rel_quot_thm = rel_quot_thm}
   4.123    in
   4.124 -    Quotmaps.map (Symtab.update (relatorT_name, minfo)) ctxt
   4.125 +    Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) ctxt
   4.126    end    
   4.127  
   4.128  val quot_map_attribute_setup =
   4.129    Attrib.setup @{binding quot_map} (Scan.succeed (Thm.declaration_attribute add_quot_map))
   4.130      "declaration of the Quotient map theorem"
   4.131  
   4.132 -fun print_quotmaps ctxt =
   4.133 +fun print_quot_maps ctxt =
   4.134    let
   4.135      fun prt_map (ty_name, {rel_quot_thm}) =
   4.136        Pretty.block (separate (Pretty.brk 2)
   4.137 @@ -118,67 +157,49 @@
   4.138            Pretty.str "quot. theorem:", 
   4.139            Syntax.pretty_term ctxt (prop_of rel_quot_thm)])
   4.140    in
   4.141 -    map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
   4.142 +    map prt_map (Symtab.dest (get_quot_maps ctxt))
   4.143      |> Pretty.big_list "maps for type constructors:"
   4.144      |> Pretty.writeln
   4.145    end
   4.146  
   4.147  (* info about quotient types *)
   4.148 -type pcrel_info = {pcrel_def: thm, pcr_cr_eq: thm}
   4.149 -type quotients = {quot_thm: thm, pcrel_info: pcrel_info option}
   4.150 -
   4.151 -structure Quotients = Generic_Data
   4.152 -(
   4.153 -  type T = quotients Symtab.table
   4.154 -  val empty = Symtab.empty
   4.155 -  val extend = I
   4.156 -  fun merge data = Symtab.merge (K true) data
   4.157 -)
   4.158 -
   4.159 -fun transform_pcrel_info phi {pcrel_def, pcr_cr_eq} =
   4.160 +fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} =
   4.161    {pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq}
   4.162  
   4.163 -fun transform_quotients phi {quot_thm, pcrel_info} =
   4.164 -  {quot_thm = Morphism.thm phi quot_thm, pcrel_info = Option.map (transform_pcrel_info phi) pcrel_info}
   4.165 +fun transform_quotient phi {quot_thm, pcr_info} =
   4.166 +  {quot_thm = Morphism.thm phi quot_thm, pcr_info = Option.map (transform_pcr_info phi) pcr_info}
   4.167  
   4.168 -val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
   4.169 -val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
   4.170 +fun lookup_quotients ctxt type_name = Symtab.lookup (get_quotients ctxt) type_name
   4.171  
   4.172 -fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))
   4.173 +fun update_quotients type_name qinfo ctxt = 
   4.174 +  Data.map (map_quotients (Symtab.update (type_name, qinfo))) ctxt
   4.175  
   4.176  fun delete_quotients quot_thm ctxt =
   4.177    let
   4.178      val (_, qtyp) = quot_thm_rty_qty quot_thm
   4.179      val qty_full_name = (fst o dest_Type) qtyp
   4.180 -    val symtab = Quotients.get ctxt
   4.181 -    val opt_stored_quot_thm = Symtab.lookup symtab qty_full_name
   4.182 +    val symtab = get_quotients' ctxt
   4.183 +    fun compare_data (_, data) = Thm.eq_thm_prop (#quot_thm data, quot_thm)
   4.184    in
   4.185 -    case opt_stored_quot_thm of
   4.186 -      SOME data => 
   4.187 -        if Thm.eq_thm_prop (#quot_thm data, quot_thm) then
   4.188 -          Quotients.map (Symtab.delete qty_full_name) ctxt
   4.189 -        else
   4.190 -          ctxt
   4.191 -      | NONE => ctxt
   4.192 +    if Symtab.member compare_data symtab (qty_full_name, quot_thm)
   4.193 +      then Data.map (map_quotients (Symtab.delete qty_full_name)) ctxt
   4.194 +      else ctxt
   4.195    end
   4.196  
   4.197 -fun dest_quotients ctxt =  (* FIXME slightly expensive way to retrieve data *)
   4.198 -  map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
   4.199 -
   4.200  fun print_quotients ctxt =
   4.201    let
   4.202 -    fun prt_quot (qty_name, {quot_thm, pcrel_info}: quotients) =
   4.203 +    fun prt_quot (qty_name, {quot_thm, pcr_info}: quotient) =
   4.204        Pretty.block (separate (Pretty.brk 2)
   4.205         [Pretty.str "type:", 
   4.206          Pretty.str qty_name,
   4.207          Pretty.str "quot. thm:",
   4.208          Syntax.pretty_term ctxt (prop_of quot_thm),
   4.209          Pretty.str "pcrel_def thm:",
   4.210 -        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcrel_def) pcrel_info,
   4.211 +        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcrel_def) pcr_info,
   4.212          Pretty.str "pcr_cr_eq thm:",
   4.213 -        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcr_cr_eq) pcrel_info])
   4.214 +        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcr_cr_eq) pcr_info])
   4.215    in
   4.216 -    map prt_quot (Symtab.dest (Quotients.get (Context.Proof ctxt)))
   4.217 +    map prt_quot (Symtab.dest (get_quotients ctxt))
   4.218      |> Pretty.big_list "quotients:"
   4.219      |> Pretty.writeln
   4.220    end
   4.221 @@ -187,6 +208,8 @@
   4.222    Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients))
   4.223      "deletes the Quotient theorem"
   4.224  
   4.225 +(* theorems that a relator of an invariant is an invariant of the corresponding predicate *)
   4.226 +
   4.227  structure Invariant_Commute = Named_Thms
   4.228  (
   4.229    val name = @{binding invariant_commute}
   4.230 @@ -197,16 +220,8 @@
   4.231  
   4.232  (* info about reflexivity rules *)
   4.233  
   4.234 -structure Reflexivity_Rule = Generic_Data
   4.235 -(
   4.236 -  type T = thm Item_Net.T
   4.237 -  val empty = Thm.full_rules
   4.238 -  val extend = I
   4.239 -  val merge = Item_Net.merge
   4.240 -)
   4.241 -
   4.242 -fun get_reflexivity_rules ctxt = ctxt
   4.243 -  |> (Item_Net.content o Reflexivity_Rule.get o Context.Proof)
   4.244 +fun get_reflexivity_rules ctxt = Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt))
   4.245 +  
   4.246  
   4.247  (* Conversion to create a reflp' variant of a reflexivity rule  *)
   4.248  fun safe_reflp_conv ct =
   4.249 @@ -219,7 +234,7 @@
   4.250        else_conv
   4.251        Conv.all_conv) ct
   4.252  
   4.253 -fun add_reflexivity_rule_raw thm = Reflexivity_Rule.map (Item_Net.update thm)
   4.254 +fun add_reflexivity_rule_raw thm = Data.map (map_reflexivity_rules (Item_Net.update thm))
   4.255  val add_reflexivity_rule_raw_attribute = Thm.declaration_attribute add_reflexivity_rule_raw
   4.256  
   4.257  fun add_reflexivity_rule thm = add_reflexivity_rule_raw thm #>
   4.258 @@ -230,40 +245,30 @@
   4.259  val relfexivity_rule_setup =
   4.260    let
   4.261      val name = @{binding reflexivity_rule}
   4.262 -    fun del_thm_raw thm = Reflexivity_Rule.map (Item_Net.remove thm)
   4.263 +    fun del_thm_raw thm = Data.map (map_reflexivity_rules (Item_Net.remove thm))
   4.264      fun del_thm thm = del_thm_raw thm #>
   4.265        del_thm_raw (Conv.fconv_rule prep_reflp_conv thm)
   4.266      val del = Thm.declaration_attribute del_thm
   4.267      val text = "rules that are used to prove that a relation is reflexive"
   4.268 -    val content = Item_Net.content o Reflexivity_Rule.get
   4.269 +    val content = Item_Net.content o get_reflexivity_rules'
   4.270    in
   4.271      Attrib.setup name (Attrib.add_del add_reflexivity_rule_attribute del) text
   4.272      #> Global_Theory.add_thms_dynamic (name, content)
   4.273    end
   4.274  
   4.275  (* info about relator distributivity theorems *)
   4.276 -type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
   4.277 -  pos_distr_rules: thm list, neg_distr_rules: thm list}
   4.278  
   4.279 -fun map_relator_distr_data f1 f2 f3 f4
   4.280 +fun map_relator_distr_data' f1 f2 f3 f4
   4.281    {pos_mono_rule, neg_mono_rule, pos_distr_rules, neg_distr_rules} =
   4.282    {pos_mono_rule   = f1 pos_mono_rule, 
   4.283     neg_mono_rule   = f2 neg_mono_rule,
   4.284     pos_distr_rules = f3 pos_distr_rules, 
   4.285     neg_distr_rules = f4 neg_distr_rules}
   4.286  
   4.287 -fun map_pos_mono_rule f = map_relator_distr_data f I I I
   4.288 -fun map_neg_mono_rule f = map_relator_distr_data I f I I
   4.289 -fun map_pos_distr_rules f = map_relator_distr_data I I f I 
   4.290 -fun map_neg_distr_rules f = map_relator_distr_data I I I f
   4.291 -
   4.292 -structure Relator_Distr = Generic_Data
   4.293 -(
   4.294 -  type T = relator_distr_data Symtab.table
   4.295 -  val empty = Symtab.empty
   4.296 -  val extend = I
   4.297 -  fun merge data = Symtab.merge (K true) data
   4.298 -);
   4.299 +fun map_pos_mono_rule f = map_relator_distr_data' f I I I
   4.300 +fun map_neg_mono_rule f = map_relator_distr_data' I f I I
   4.301 +fun map_pos_distr_rules f = map_relator_distr_data' I I f I 
   4.302 +fun map_neg_distr_rules f = map_relator_distr_data' I I I f
   4.303  
   4.304  fun introduce_polarities rule =
   4.305    let
   4.306 @@ -315,14 +320,14 @@
   4.307      val mono_rule = introduce_polarities mono_rule
   4.308      val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 
   4.309        dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) mono_rule
   4.310 -    val _ = if Symtab.defined (Relator_Distr.get ctxt) mono_ruleT_name 
   4.311 +    val _ = if Symtab.defined (get_relator_distr_data' ctxt) mono_ruleT_name 
   4.312        then error ("Monotocity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.")
   4.313        else ()
   4.314      val neg_mono_rule = negate_mono_rule mono_rule
   4.315      val relator_distr_data = {pos_mono_rule = mono_rule, neg_mono_rule = neg_mono_rule, 
   4.316        pos_distr_rules = [], neg_distr_rules = []}
   4.317    in
   4.318 -    Relator_Distr.map (Symtab.update (mono_ruleT_name, relator_distr_data)) ctxt
   4.319 +    Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data))) ctxt
   4.320    end;
   4.321  
   4.322  local 
   4.323 @@ -331,8 +336,9 @@
   4.324        val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 
   4.325          dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) distr_rule
   4.326      in
   4.327 -      if Symtab.defined (Relator_Distr.get ctxt) distr_ruleT_name then 
   4.328 -        Relator_Distr.map (Symtab.map_entry distr_ruleT_name (update_entry distr_rule)) ctxt
   4.329 +      if Symtab.defined (get_relator_distr_data' ctxt) distr_ruleT_name then 
   4.330 +        Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule))) 
   4.331 +          ctxt
   4.332        else error "The monoticity rule is not defined."
   4.333      end
   4.334  
   4.335 @@ -425,14 +431,13 @@
   4.336  
   4.337  fun get_distr_rules_raw ctxt = Symtab.fold 
   4.338    (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules) 
   4.339 -    (Relator_Distr.get ctxt) []
   4.340 +    (get_relator_distr_data' ctxt) []
   4.341  
   4.342  fun get_mono_rules_raw ctxt = Symtab.fold 
   4.343    (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules) 
   4.344 -    (Relator_Distr.get ctxt) []
   4.345 +    (get_relator_distr_data' ctxt) []
   4.346  
   4.347 -val lookup_relator_distr_data = Symtab.lookup o Relator_Distr.get o Context.Proof
   4.348 -val lookup_relator_distr_data_global = Symtab.lookup o Relator_Distr.get o Context.Theory
   4.349 +val lookup_relator_distr_data = Symtab.lookup o get_relator_distr_data
   4.350  
   4.351  val relator_distr_attribute_setup =
   4.352    Attrib.setup @{binding relator_mono} (Scan.succeed (Thm.declaration_attribute add_mono_rule))
   4.353 @@ -456,8 +461,8 @@
   4.354  (* outer syntax commands *)
   4.355  
   4.356  val _ =
   4.357 -  Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions"
   4.358 -    (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
   4.359 +  Outer_Syntax.improper_command @{command_spec "print_quot_maps"} "print quotient map functions"
   4.360 +    (Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of)))
   4.361  
   4.362  val _ =
   4.363    Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
     5.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Aug 28 11:15:14 2013 +0200
     5.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Aug 28 14:37:35 2013 +0200
     5.3 @@ -201,12 +201,12 @@
     5.4      val (pcr_cr_eq, lthy) = case pcrel_def of
     5.5        SOME pcrel_def => apfst SOME (define_pcr_cr_eq lthy pcrel_def)
     5.6        | NONE => (NONE, lthy)
     5.7 -    val pcrel_info = case pcrel_def of
     5.8 +    val pcr_info = case pcrel_def of
     5.9        SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq }
    5.10        | NONE => NONE
    5.11 -    val quotients = { quot_thm = quot_thm, pcrel_info = pcrel_info }
    5.12 +    val quotients = { quot_thm = quot_thm, pcr_info = pcr_info }
    5.13      val qty_full_name = (fst o dest_Type) qtyp  
    5.14 -    fun quot_info phi = Lifting_Info.transform_quotients phi quotients
    5.15 +    fun quot_info phi = Lifting_Info.transform_quotient phi quotients
    5.16      val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
    5.17      val lthy = case opt_reflp_thm of
    5.18        SOME reflp_thm => lthy
    5.19 @@ -376,7 +376,7 @@
    5.20        reduced_assm RS thm
    5.21      end
    5.22  in
    5.23 -  fun parametrize_domain dom_thm (pcrel_info : Lifting_Info.pcrel_info) ctxt =
    5.24 +  fun parametrize_domain dom_thm (pcr_info : Lifting_Info.pcr) ctxt =
    5.25      let
    5.26        fun reduce_first_assm ctxt rules thm =
    5.27          let
    5.28 @@ -386,9 +386,9 @@
    5.29            reduced_assm RS thm
    5.30          end
    5.31  
    5.32 -      val pcr_cr_met_eq = #pcr_cr_eq pcrel_info RS @{thm eq_reflection}
    5.33 +      val pcr_cr_met_eq = #pcr_cr_eq pcr_info RS @{thm eq_reflection}
    5.34        val pcr_Domainp_eq = rewrite_first_Domainp_arg (Thm.symmetric pcr_cr_met_eq) dom_thm
    5.35 -      val pcrel_def = #pcrel_def pcrel_info
    5.36 +      val pcrel_def = #pcrel_def pcr_info
    5.37        val pcr_Domainp_par_left_total = 
    5.38          (dom_thm RS @{thm pcr_Domainp_par_left_total})
    5.39            |> fold_Domainp_pcrel pcrel_def
    5.40 @@ -422,7 +422,7 @@
    5.41  end
    5.42  
    5.43  fun get_pcrel_info ctxt qty_full_name =  
    5.44 -  #pcrel_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
    5.45 +  #pcr_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
    5.46  
    5.47  fun get_Domainp_thm quot_thm =
    5.48     the (get_first (try(curry op RS quot_thm)) [@{thm invariant_to_Domainp}, @{thm Quotient_to_Domainp}])
     6.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Wed Aug 28 11:15:14 2013 +0200
     6.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Wed Aug 28 14:37:35 2013 +0200
     6.3 @@ -75,8 +75,8 @@
     6.4    end
     6.5  
     6.6  fun get_pcrel_info ctxt s =
     6.7 -  case #pcrel_info (get_quot_data ctxt s) of
     6.8 -    SOME pcrel_info => pcrel_info
     6.9 +  case #pcr_info (get_quot_data ctxt s) of
    6.10 +    SOME pcr_info => pcr_info
    6.11    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    6.12      [Pretty.str ("No parametrized correspondce relation for " ^ quote s), 
    6.13       Pretty.brk 1, 
    6.14 @@ -100,7 +100,7 @@
    6.15     let
    6.16      val thy = Proof_Context.theory_of ctxt
    6.17    in
    6.18 -    (case Lifting_Info.lookup_quotmaps ctxt s of
    6.19 +    (case Lifting_Info.lookup_quot_maps ctxt s of
    6.20        SOME map_data => Thm.transfer thy (#rel_quot_thm map_data)
    6.21      | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    6.22        [Pretty.str ("No relator for the type " ^ quote s),