src/HOL/Tools/Quotient/quotient_term.ML

 end;
 
 structure Quotient_Term: QUOTIENT_TERM =
 struct
 
-open Quotient_Info;
-
 exception LIFT_MATCH of string
 
 
 
 (*** Aggregate Rep/Abs Function ***)

   | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
 
 fun get_mapfun ctxt s =
   let
     val thy = ProofContext.theory_of ctxt
-    val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound =>
+    val mapfun = #mapfun (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
       raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
   in
     Const (mapfun, dummyT)
   end
 

    a quotient definition
 *)
 fun get_rty_qty ctxt s =
   let
     val thy = ProofContext.theory_of ctxt
-    val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound =>
+    val qdata = Quotient_Info.quotdata_lookup thy s handle Quotient_Info.NotFound =>
       raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
   in
     (#rtyp qdata, #qtyp qdata)
   end
 

   Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
 
 fun get_relmap ctxt s =
   let
     val thy = ProofContext.theory_of ctxt
-    val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound =>
+    val relmap = #relmap (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
       raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
   in
     Const (relmap, dummyT)
   end
 

 
 fun get_equiv_rel ctxt s =
   let
     val thy = ProofContext.theory_of ctxt
   in
-    #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound =>
+    #equiv_rel (Quotient_Info.quotdata_lookup thy s) handle Quotient_Info.NotFound =>
       raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
   end
 
 fun equiv_match_err ctxt ty_pat ty =
   let

       (Type (rs, rtys), Type (qs, qtys)) =>
         if rs = qs then
           if length rtys <> length qtys then false
           else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
         else
-          (case quotdata_lookup_raw thy qs of
+          (case Quotient_Info.quotdata_lookup_raw thy qs of
             SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
           | NONE => false)
     | _ => false)
 
 

           | same_const _ _ = false
       in
         if same_const rtrm qtrm then rtrm
         else
           let
-            val rtrm' = #rconst (qconsts_lookup thy qtrm)
+            val rtrm' = #rconst (Quotient_Info.qconsts_lookup thy qtrm)
               handle Quotient_Info.NotFound =>
                 term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
           in
             if Pattern.matches thy (rtrm', rtrm)
             then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm

 *)
 fun mk_ty_subst qtys direction ctxt =
   let
     val thy = ProofContext.theory_of ctxt
   in
-    quotdata_dest ctxt
+    Quotient_Info.quotdata_dest ctxt
     |> map (fn x => (#rtyp x, #qtyp x))
     |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
     |> map (if direction then swap else I)
   end
 

   let
     val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt)
     fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
 
     val const_substs =
-      qconsts_dest ctxt
+      Quotient_Info.qconsts_dest ctxt
       |> map (fn x => (#rconst x, #qconst x))
       |> map (if direction then swap else I)
 
     val rel_substs =
-      quotdata_dest ctxt
+      Quotient_Info.quotdata_dest ctxt
       |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
       |> map (if direction then swap else I)
   in
     filter proper (const_substs @ rel_substs)
   end