use Thm.transfer for thms stored in generic context data storage
authorkuncar
Fri Mar 23 22:00:17 2012 +0100 (2012-03-23)
changeset 47106dfa5ed8d94b4
parent 47105 e64ffc96a49f
child 47107 35807a5d8dc2
use Thm.transfer for thms stored in generic context data storage
src/HOL/Tools/Quotient/quotient_term.ML
     1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 23 18:23:47 2012 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 23 22:00:17 2012 +0100
     1.3 @@ -336,19 +336,25 @@
     1.4  
     1.5  (* generation of the Quotient theorem  *)
     1.6  
     1.7 +exception CODE_GEN of string
     1.8 +
     1.9  fun get_quot_thm ctxt s =
    1.10    let
    1.11      val thy = Proof_Context.theory_of ctxt
    1.12    in
    1.13 -    (case Quotient_Info.lookup_quotients_global thy s of
    1.14 -      SOME qdata => #quot_thm qdata
    1.15 -    | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
    1.16 +    (case Quotient_Info.lookup_quotients ctxt s of
    1.17 +      SOME qdata => Thm.transfer thy (#quot_thm qdata)
    1.18 +    | NONE => raise CODE_GEN ("No quotient type " ^ quote s ^ " found."))
    1.19    end
    1.20  
    1.21 -fun get_rel_quot_thm thy s =
    1.22 -  (case Quotient_Info.lookup_quotmaps thy s of
    1.23 -    SOME map_data => #quot_thm map_data
    1.24 -  | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"));
    1.25 +fun get_rel_quot_thm ctxt s =
    1.26 +   let
    1.27 +    val thy = Proof_Context.theory_of ctxt
    1.28 +  in
    1.29 +    (case Quotient_Info.lookup_quotmaps ctxt s of
    1.30 +      SOME map_data => Thm.transfer thy (#quot_thm map_data)
    1.31 +    | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")"))
    1.32 +  end
    1.33  
    1.34  fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
    1.35