src/HOL/Tools/Quotient/quotient_term.ML
changeset 42361 23f352990944
parent 41451 892e67be8304
child 44413 80d460bc6fa8
     1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4  
     1.5  fun get_mapfun ctxt s =
     1.6    let
     1.7 -    val thy = ProofContext.theory_of ctxt
     1.8 +    val thy = Proof_Context.theory_of ctxt
     1.9      val mapfun = #mapfun (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
    1.10        raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
    1.11    in
    1.12 @@ -101,7 +101,7 @@
    1.13  *)
    1.14  fun get_rty_qty ctxt s =
    1.15    let
    1.16 -    val thy = ProofContext.theory_of ctxt
    1.17 +    val thy = Proof_Context.theory_of ctxt
    1.18      val qdata = Quotient_Info.quotdata_lookup thy s handle Quotient_Info.NotFound =>
    1.19        raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
    1.20    in
    1.21 @@ -122,7 +122,7 @@
    1.22  (* matches a type pattern with a type *)
    1.23  fun match ctxt err ty_pat ty =
    1.24    let
    1.25 -    val thy = ProofContext.theory_of ctxt
    1.26 +    val thy = Proof_Context.theory_of ctxt
    1.27    in
    1.28      Sign.typ_match thy (ty_pat, ty) Vartab.empty
    1.29        handle Type.TYPE_MATCH => err ctxt ty_pat ty
    1.30 @@ -258,7 +258,7 @@
    1.31  (* instantiates TVars so that the term is of type ty *)
    1.32  fun force_typ ctxt trm ty =
    1.33    let
    1.34 -    val thy = ProofContext.theory_of ctxt
    1.35 +    val thy = Proof_Context.theory_of ctxt
    1.36      val trm_ty = fastype_of trm
    1.37      val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
    1.38    in
    1.39 @@ -273,7 +273,7 @@
    1.40  
    1.41  fun get_relmap ctxt s =
    1.42    let
    1.43 -    val thy = ProofContext.theory_of ctxt
    1.44 +    val thy = Proof_Context.theory_of ctxt
    1.45      val relmap = #relmap (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
    1.46        raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
    1.47    in
    1.48 @@ -296,7 +296,7 @@
    1.49  
    1.50  fun get_equiv_rel ctxt s =
    1.51    let
    1.52 -    val thy = ProofContext.theory_of ctxt
    1.53 +    val thy = Proof_Context.theory_of ctxt
    1.54    in
    1.55      #equiv_rel (Quotient_Info.quotdata_lookup thy s) handle Quotient_Info.NotFound =>
    1.56        raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
    1.57 @@ -554,7 +554,7 @@
    1.58  
    1.59    | (_, Const _) =>
    1.60        let
    1.61 -        val thy = ProofContext.theory_of ctxt
    1.62 +        val thy = Proof_Context.theory_of ctxt
    1.63          fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
    1.64            | same_const _ _ = false
    1.65        in
    1.66 @@ -707,7 +707,7 @@
    1.67    case rty of
    1.68      Type (s, rtys) =>
    1.69        let
    1.70 -        val thy = ProofContext.theory_of ctxt
    1.71 +        val thy = Proof_Context.theory_of ctxt
    1.72          val rty' = Type (s, map (subst_typ ctxt ty_subst) rtys)
    1.73  
    1.74          fun matches [] = rty'
    1.75 @@ -729,7 +729,7 @@
    1.76    | Bound i => Bound i
    1.77    | Const (a, ty) =>
    1.78        let
    1.79 -        val thy = ProofContext.theory_of ctxt
    1.80 +        val thy = Proof_Context.theory_of ctxt
    1.81  
    1.82          fun matches [] = Const (a, subst_typ ctxt ty_subst ty)
    1.83            | matches ((rconst, qconst)::tail) =
    1.84 @@ -749,7 +749,7 @@
    1.85  *)
    1.86  fun mk_ty_subst qtys direction ctxt =
    1.87    let
    1.88 -    val thy = ProofContext.theory_of ctxt
    1.89 +    val thy = Proof_Context.theory_of ctxt
    1.90    in
    1.91      Quotient_Info.quotdata_dest ctxt
    1.92      |> map (fn x => (#rtyp x, #qtyp x))