localized quotient data;
authorwenzelm
Thu Oct 27 21:02:10 2011 +0200 (2011-10-27)
changeset 452809fd6fce8a230
parent 45279 89a17197cb98
child 45281 29e88714ffe4
localized quotient data;
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Quotient/quotient_info.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/Quotient/quotient_typ.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Oct 27 20:26:38 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Oct 27 21:02:10 2011 +0200
     1.3 @@ -641,17 +641,15 @@
     1.4      s |> AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
     1.5        |> Option.map snd |> these |> null |> not
     1.6    | is_codatatype _ _ = false
     1.7 -fun is_real_quot_type thy (Type (s, _)) =
     1.8 -    is_some (Quotient_Info.lookup_quotients thy s)
     1.9 +fun is_real_quot_type ctxt (Type (s, _)) =
    1.10 +    is_some (Quotient_Info.lookup_quotients ctxt s)
    1.11    | is_real_quot_type _ _ = false
    1.12  fun is_quot_type ctxt T =
    1.13 -  let val thy = Proof_Context.theory_of ctxt in
    1.14 -    is_real_quot_type thy T andalso not (is_codatatype ctxt T)
    1.15 -  end
    1.16 +    is_real_quot_type ctxt T andalso not (is_codatatype ctxt T)
    1.17  fun is_pure_typedef ctxt (T as Type (s, _)) =
    1.18      let val thy = Proof_Context.theory_of ctxt in
    1.19        is_typedef ctxt s andalso
    1.20 -      not (is_real_datatype thy s orelse is_real_quot_type thy T orelse
    1.21 +      not (is_real_datatype thy s orelse is_real_quot_type ctxt T orelse
    1.22             is_codatatype ctxt T orelse is_record_type T orelse
    1.23             is_integer_like_type T)
    1.24      end
    1.25 @@ -682,7 +680,7 @@
    1.26  fun is_datatype ctxt stds (T as Type (s, _)) =
    1.27      let val thy = Proof_Context.theory_of ctxt in
    1.28        (is_typedef ctxt s orelse is_codatatype ctxt T orelse
    1.29 -       T = @{typ ind} orelse is_real_quot_type thy T) andalso
    1.30 +       T = @{typ ind} orelse is_real_quot_type ctxt T) andalso
    1.31        not (is_basic_datatype thy stds s)
    1.32      end
    1.33    | is_datatype _ _ _ = false
    1.34 @@ -737,8 +735,11 @@
    1.35         SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
    1.36       | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
    1.37    | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
    1.38 -fun rep_type_for_quot_type thy (T as Type (s, _)) =
    1.39 -    let val {qtyp, rtyp, ...} = the (Quotient_Info.lookup_quotients thy s) in
    1.40 +fun rep_type_for_quot_type ctxt (T as Type (s, _)) =
    1.41 +    let
    1.42 +      val thy = Proof_Context.theory_of ctxt
    1.43 +      val {qtyp, rtyp, ...} = the (Quotient_Info.lookup_quotients ctxt s)
    1.44 +    in
    1.45        instantiate_type thy qtyp T rtyp
    1.46      end
    1.47    | rep_type_for_quot_type _ T =
    1.48 @@ -912,8 +913,8 @@
    1.49                 val T' = (Record.get_extT_fields thy T
    1.50                          |> apsnd single |> uncurry append |> map snd) ---> T
    1.51               in [(s', T')] end
    1.52 -           else if is_real_quot_type thy T then
    1.53 -             [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
    1.54 +           else if is_real_quot_type ctxt T then
    1.55 +             [(@{const_name Quot}, rep_type_for_quot_type ctxt T --> T)]
    1.56             else case typedef_info ctxt s of
    1.57               SOME {abs_type, rep_type, Abs_name, ...} =>
    1.58               [(Abs_name,
    1.59 @@ -1760,7 +1761,7 @@
    1.60                        val rep_T = domain_type (range_type T)
    1.61                        val (rep_fun, _) = quot_rep_of depth Ts abs_T rep_T []
    1.62                        val (equiv_rel, _) =
    1.63 -                        equiv_relation_for_quot_type thy abs_T
    1.64 +                        equiv_relation_for_quot_type ctxt abs_T
    1.65                      in
    1.66                        (Abs (Name.uu, abs_T, equiv_rel $ (rep_fun $ Bound 0)),
    1.67                         ts)
    1.68 @@ -1912,10 +1913,9 @@
    1.69    end
    1.70  fun optimized_quot_type_axioms ctxt stds abs_z =
    1.71    let
    1.72 -    val thy = Proof_Context.theory_of ctxt
    1.73      val abs_T = Type abs_z
    1.74 -    val rep_T = rep_type_for_quot_type thy abs_T
    1.75 -    val (equiv_rel, partial) = equiv_relation_for_quot_type thy abs_T
    1.76 +    val rep_T = rep_type_for_quot_type ctxt abs_T
    1.77 +    val (equiv_rel, partial) = equiv_relation_for_quot_type ctxt abs_T
    1.78      val a_var = Var (("a", 0), abs_T)
    1.79      val x_var = Var (("x", 0), rep_T)
    1.80      val y_var = Var (("y", 0), rep_T)
     2.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 20:26:38 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 21:02:10 2011 +0200
     2.3 @@ -7,23 +7,19 @@
     2.4  signature QUOTIENT_INFO =
     2.5  sig
     2.6    type quotmaps = {mapfun: string, relmap: string}
     2.7 -  val lookup_quotmaps: theory -> string -> quotmaps option
     2.8 -  val update_quotmaps_global: string -> quotmaps -> theory -> theory
     2.9 -  val update_quotmaps: string -> quotmaps -> Proof.context -> Proof.context
    2.10 +  val lookup_quotmaps: Proof.context -> string -> quotmaps option
    2.11    val print_quotmaps: Proof.context -> unit
    2.12  
    2.13    type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
    2.14    val transform_quotients: morphism -> quotients -> quotients
    2.15 -  val lookup_quotients: theory -> string -> quotients option
    2.16 -  val update_quotients_global: string -> quotients -> theory -> theory
    2.17 +  val lookup_quotients: Proof.context -> string -> quotients option
    2.18    val update_quotients: string -> quotients -> Context.generic -> Context.generic
    2.19    val dest_quotients: Proof.context -> quotients list
    2.20    val print_quotients: Proof.context -> unit
    2.21  
    2.22    type quotconsts = {qconst: term, rconst: term, def: thm}
    2.23    val transform_quotconsts: morphism -> quotconsts -> quotconsts
    2.24 -  val lookup_quotconsts: theory -> term -> quotconsts option
    2.25 -  val update_quotconsts_global: string -> quotconsts -> theory -> theory
    2.26 +  val lookup_quotconsts: Proof.context -> term -> quotconsts option
    2.27    val update_quotconsts: string -> quotconsts -> Context.generic -> Context.generic
    2.28    val dest_quotconsts: Proof.context -> quotconsts list
    2.29    val print_quotconsts: Proof.context -> unit
    2.30 @@ -50,7 +46,7 @@
    2.31  (* info about map- and rel-functions for a type *)
    2.32  type quotmaps = {mapfun: string, relmap: string}
    2.33  
    2.34 -structure Quotmaps = Theory_Data
    2.35 +structure Quotmaps = Generic_Data
    2.36  (
    2.37    type T = quotmaps Symtab.table
    2.38    val empty = Symtab.empty
    2.39 @@ -58,29 +54,23 @@
    2.40    fun merge data = Symtab.merge (K true) data
    2.41  )
    2.42  
    2.43 -val lookup_quotmaps = Symtab.lookup o Quotmaps.get
    2.44 -
    2.45 -fun update_quotmaps_global k minfo = Quotmaps.map (Symtab.update (k, minfo))
    2.46 -fun update_quotmaps k minfo = Proof_Context.background_theory (update_quotmaps_global k minfo)  (* FIXME !? *)
    2.47 +val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof
    2.48  
    2.49 -fun maps_attribute_aux s minfo = Thm.declaration_attribute
    2.50 -  (fn _ => Context.mapping (update_quotmaps_global s minfo) (update_quotmaps s minfo))
    2.51 -
    2.52 -(* attribute to be used in declare statements *)
    2.53 -fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =
    2.54 +fun quotmaps_attribute (ctxt, (tystr, (mapstr, relstr))) =
    2.55    let
    2.56 -    val thy = Proof_Context.theory_of ctxt
    2.57 -    val tyname = Sign.intern_type thy tystr  (* FIXME pass proper internal names *)
    2.58 +    val thy = Proof_Context.theory_of ctxt  (* FIXME proper local context *)
    2.59 +    val tyname = Sign.intern_type thy tystr  (* FIXME pass proper internal names via syntax *)
    2.60      val mapname = Sign.intern_const thy mapstr
    2.61      val relname = Sign.intern_const thy relstr
    2.62  
    2.63      fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())
    2.64      val _ = List.app sanity_check [mapname, relname]
    2.65 +    val minfo = {mapfun = mapname, relmap = relname}
    2.66    in
    2.67 -    maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
    2.68 +    Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo)))
    2.69    end
    2.70  
    2.71 -val maps_attr_parser =
    2.72 +val quotmaps_attr_parser =
    2.73    Args.context -- Scan.lift
    2.74      ((Args.name --| Parse.$$$ "=") --
    2.75        (Parse.$$$ "(" |-- Args.name --| Parse.$$$ "," --
    2.76 @@ -95,9 +85,7 @@
    2.77            "map:", mapfun,
    2.78            "relation map:", relmap]))
    2.79    in
    2.80 -    Quotmaps.get (Proof_Context.theory_of ctxt)
    2.81 -    |> Symtab.dest
    2.82 -    |> map (prt_map)
    2.83 +    map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
    2.84      |> Pretty.big_list "maps for type constructors:"
    2.85      |> Pretty.writeln
    2.86    end
    2.87 @@ -106,7 +94,7 @@
    2.88  (* info about quotient types *)
    2.89  type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
    2.90  
    2.91 -structure Quotients = Theory_Data
    2.92 +structure Quotients = Generic_Data
    2.93  (
    2.94    type T = quotients Symtab.table
    2.95    val empty = Symtab.empty
    2.96 @@ -120,13 +108,12 @@
    2.97     equiv_rel = Morphism.term phi equiv_rel,
    2.98     equiv_thm = Morphism.thm phi equiv_thm}
    2.99  
   2.100 -val lookup_quotients = Symtab.lookup o Quotients.get
   2.101 +val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
   2.102  
   2.103 -fun update_quotients_global str qinfo = Quotients.map (Symtab.update (str, qinfo))
   2.104 -fun update_quotients str qinfo = Context.mapping (update_quotients_global str qinfo) I  (* FIXME !? *)
   2.105 +fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))
   2.106  
   2.107 -fun dest_quotients lthy =  (* FIXME slightly expensive way to retrieve data *)
   2.108 -  map snd (Symtab.dest (Quotients.get (Proof_Context.theory_of lthy)))  (* FIXME !? *)
   2.109 +fun dest_quotients ctxt =  (* FIXME slightly expensive way to retrieve data *)
   2.110 +  map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
   2.111  
   2.112  fun print_quotients ctxt =
   2.113    let
   2.114 @@ -141,9 +128,7 @@
   2.115          Pretty.str "equiv. thm:",
   2.116          Syntax.pretty_term ctxt (prop_of equiv_thm)])
   2.117    in
   2.118 -    Quotients.get (Proof_Context.theory_of ctxt)
   2.119 -    |> Symtab.dest
   2.120 -    |> map (prt_quot o snd)
   2.121 +    map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt)))
   2.122      |> Pretty.big_list "quotients:"
   2.123      |> Pretty.writeln
   2.124    end
   2.125 @@ -157,7 +142,7 @@
   2.126  (* We need to be able to lookup instances of lifted constants,
   2.127     for example given "nat fset" we need to find "'a fset";
   2.128     but overloaded constants share the same name *)
   2.129 -structure Quotconsts = Theory_Data
   2.130 +structure Quotconsts = Generic_Data
   2.131  (
   2.132    type T = quotconsts list Symtab.table
   2.133    val empty = Symtab.empty
   2.134 @@ -170,23 +155,21 @@
   2.135     rconst = Morphism.term phi rconst,
   2.136     def = Morphism.thm phi def}
   2.137  
   2.138 -fun update_quotconsts_global name qcinfo = Quotconsts.map (Symtab.cons_list (name, qcinfo))
   2.139 -fun update_quotconsts name qcinfo = Context.mapping (update_quotconsts_global name qcinfo) I  (* FIXME !? *)
   2.140 +fun update_quotconsts name qcinfo = Quotconsts.map (Symtab.cons_list (name, qcinfo))
   2.141 +
   2.142 +fun dest_quotconsts ctxt =
   2.143 +  flat (map snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
   2.144  
   2.145 -fun dest_quotconsts lthy =
   2.146 -  flat (map snd (Symtab.dest (Quotconsts.get (Proof_Context.theory_of lthy))))  (* FIXME !? *)
   2.147 +fun lookup_quotconsts ctxt t =
   2.148 +  let
   2.149 +    val thy = Proof_Context.theory_of ctxt
   2.150  
   2.151 -fun lookup_quotconsts thy t =
   2.152 -  let
   2.153      val (name, qty) = dest_Const t
   2.154      fun matches (x: quotconsts) =
   2.155 -      let
   2.156 -        val (name', qty') = dest_Const (#qconst x);
   2.157 -      in
   2.158 -        name = name' andalso Sign.typ_instance thy (qty, qty')
   2.159 -      end
   2.160 +      let val (name', qty') = dest_Const (#qconst x);
   2.161 +      in name = name' andalso Sign.typ_instance thy (qty, qty') end
   2.162    in
   2.163 -    (case Symtab.lookup (Quotconsts.get thy) name of
   2.164 +    (case Symtab.lookup (Quotconsts.get (Context.Proof ctxt)) name of
   2.165        NONE => NONE
   2.166      | SOME l => find_first matches l)
   2.167    end
   2.168 @@ -201,11 +184,7 @@
   2.169          Pretty.str "as",
   2.170          Syntax.pretty_term ctxt (prop_of def)])
   2.171    in
   2.172 -    Quotconsts.get (Proof_Context.theory_of ctxt)
   2.173 -    |> Symtab.dest
   2.174 -    |> map snd
   2.175 -    |> flat
   2.176 -    |> map prt_qconst
   2.177 +    map prt_qconst (maps snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
   2.178      |> Pretty.big_list "quotient constants:"
   2.179      |> Pretty.writeln
   2.180    end
   2.181 @@ -263,7 +242,7 @@
   2.182  (* theory setup *)
   2.183  
   2.184  val setup =
   2.185 -  Attrib.setup @{binding map} (maps_attr_parser >> maps_attribute)
   2.186 +  Attrib.setup @{binding map} (quotmaps_attr_parser >> quotmaps_attribute)
   2.187      "declaration of map information" #>
   2.188    Equiv_Rules.setup #>
   2.189    Rsp_Rules.setup #>
   2.190 @@ -286,5 +265,4 @@
   2.191    Outer_Syntax.improper_command "print_quotconsts" "print quotient constants" Keyword.diag
   2.192      (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
   2.193  
   2.194 -
   2.195  end;
     3.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 20:26:38 2011 +0200
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 21:02:10 2011 +0200
     3.3 @@ -63,7 +63,7 @@
     3.4    | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
     3.5  
     3.6  fun get_mapfun ctxt s =
     3.7 -  (case Quotient_Info.lookup_quotmaps (Proof_Context.theory_of ctxt) s of
     3.8 +  (case Quotient_Info.lookup_quotmaps ctxt s of
     3.9      SOME map_data => Const (#mapfun map_data, dummyT)
    3.10    | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found."))
    3.11  
    3.12 @@ -96,9 +96,9 @@
    3.13     a quotient definition
    3.14  *)
    3.15  fun get_rty_qty ctxt s =
    3.16 -  case Quotient_Info.lookup_quotients (Proof_Context.theory_of ctxt) s of
    3.17 +  (case Quotient_Info.lookup_quotients ctxt s of
    3.18      SOME qdata => (#rtyp qdata, #qtyp qdata)
    3.19 -  | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.");
    3.20 +  | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
    3.21  
    3.22  (* takes two type-environments and looks
    3.23     up in both of them the variable v, which
    3.24 @@ -271,7 +271,7 @@
    3.25    Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
    3.26  
    3.27  fun get_relmap ctxt s =
    3.28 -  (case Quotient_Info.lookup_quotmaps (Proof_Context.theory_of ctxt) s of
    3.29 +  (case Quotient_Info.lookup_quotmaps ctxt s of
    3.30      SOME map_data => Const (#relmap map_data, dummyT)
    3.31    | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"))
    3.32  
    3.33 @@ -290,7 +290,7 @@
    3.34    end
    3.35  
    3.36  fun get_equiv_rel ctxt s =
    3.37 -  (case Quotient_Info.lookup_quotients (Proof_Context.theory_of ctxt) s of
    3.38 +  (case Quotient_Info.lookup_quotients ctxt s of
    3.39      SOME qdata => #equiv_rel qdata
    3.40    | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")"))
    3.41  
    3.42 @@ -418,17 +418,18 @@
    3.43  
    3.44  (* Checks that two types match, for example:
    3.45       rty -> rty   matches   qty -> qty *)
    3.46 -fun matches_typ thy rT qT =
    3.47 +fun matches_typ ctxt rT qT =
    3.48    if rT = qT then true
    3.49    else
    3.50      (case (rT, qT) of
    3.51        (Type (rs, rtys), Type (qs, qtys)) =>
    3.52          if rs = qs then
    3.53            if length rtys <> length qtys then false
    3.54 -          else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
    3.55 +          else forall (fn x => x = true) (map2 (matches_typ ctxt) rtys qtys)
    3.56          else
    3.57 -          (case Quotient_Info.lookup_quotients thy qs of
    3.58 -            SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
    3.59 +          (case Quotient_Info.lookup_quotients ctxt qs of
    3.60 +            SOME quotinfo =>
    3.61 +              Sign.typ_instance (Proof_Context.theory_of ctxt) (rT, #rtyp quotinfo)
    3.62            | NONE => false)
    3.63      | _ => false)
    3.64  
    3.65 @@ -441,7 +442,7 @@
    3.66       special treatment of bound variables
    3.67  *)
    3.68  fun regularize_trm ctxt (rtrm, qtrm) =
    3.69 -  case (rtrm, qtrm) of
    3.70 +  (case (rtrm, qtrm) of
    3.71      (Abs (x, ty, t), Abs (_, ty', t')) =>
    3.72        let
    3.73          val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
    3.74 @@ -449,6 +450,7 @@
    3.75          if ty = ty' then subtrm
    3.76          else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
    3.77        end
    3.78 +
    3.79    | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
    3.80        let
    3.81          val subtrm = regularize_trm ctxt (t, t')
    3.82 @@ -547,14 +549,14 @@
    3.83    | (_, Const _) =>
    3.84        let
    3.85          val thy = Proof_Context.theory_of ctxt
    3.86 -        fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
    3.87 +        fun same_const (Const (s, T)) (Const (s', T')) = s = s' andalso matches_typ ctxt T T'
    3.88            | same_const _ _ = false
    3.89        in
    3.90          if same_const rtrm qtrm then rtrm
    3.91          else
    3.92            let
    3.93              val rtrm' =
    3.94 -              (case Quotient_Info.lookup_quotconsts thy qtrm of
    3.95 +              (case Quotient_Info.lookup_quotconsts ctxt qtrm of
    3.96                  SOME qconst_info => #rconst qconst_info
    3.97                | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm)
    3.98            in
    3.99 @@ -584,7 +586,7 @@
   3.100          val qtrm_str = Syntax.string_of_term ctxt qtrm
   3.101        in
   3.102          raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
   3.103 -      end
   3.104 +      end)
   3.105  
   3.106  fun regularize_trm_chk ctxt (rtrm, qtrm) =
   3.107    regularize_trm ctxt (rtrm, qtrm)
   3.108 @@ -705,9 +707,9 @@
   3.109  
   3.110          fun matches [] = rty'
   3.111            | matches ((rty, qty)::tail) =
   3.112 -              case try (Sign.typ_match thy (rty, rty')) Vartab.empty of
   3.113 +              (case try (Sign.typ_match thy (rty, rty')) Vartab.empty of
   3.114                  NONE => matches tail
   3.115 -              | SOME inst => Envir.subst_type inst qty
   3.116 +              | SOME inst => Envir.subst_type inst qty)
   3.117        in
   3.118          matches ty_subst
   3.119        end
   3.120 @@ -726,9 +728,9 @@
   3.121  
   3.122          fun matches [] = Const (a, subst_typ ctxt ty_subst ty)
   3.123            | matches ((rconst, qconst)::tail) =
   3.124 -              case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
   3.125 +              (case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
   3.126                  NONE => matches tail
   3.127 -              | SOME inst => Envir.subst_term inst qconst
   3.128 +              | SOME inst => Envir.subst_term inst qconst)
   3.129        in
   3.130          matches trm_subst
   3.131        end
     4.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Oct 27 20:26:38 2011 +0200
     4.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Oct 27 21:02:10 2011 +0200
     4.3 @@ -219,13 +219,11 @@
     4.4  (* check for existence of map functions *)
     4.5  fun map_check ctxt (_, (rty, _, _)) =
     4.6    let
     4.7 -    val thy = Proof_Context.theory_of ctxt
     4.8 -
     4.9      fun map_check_aux rty warns =
    4.10 -      case rty of
    4.11 +      (case rty of
    4.12          Type (_, []) => warns
    4.13 -      | Type (s, _) => if is_some (Quotient_Info.lookup_quotmaps thy s) then warns else s :: warns
    4.14 -      | _ => warns
    4.15 +      | Type (s, _) => if is_some (Quotient_Info.lookup_quotmaps ctxt s) then warns else s :: warns
    4.16 +      | _ => warns)
    4.17  
    4.18      val warns = map_check_aux rty []
    4.19    in
    4.20 @@ -310,4 +308,4 @@
    4.21      "quotient type definitions (require equivalence proofs)"
    4.22         Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
    4.23  
    4.24 -end; (* structure *)
    4.25 +end;