avoid potential problem with stale theory
authorhaftmann
Wed May 20 12:09:07 2009 +0200 (2009-05-20)
changeset 31210d6681ddc046c
parent 31209 77da3aad5917
child 31211 ba0ad1c020ee
avoid potential problem with stale theory
src/Pure/Isar/class_target.ML
src/Pure/axclass.ML
     1.1 --- a/src/Pure/Isar/class_target.ML	Wed May 20 10:37:38 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Wed May 20 12:09:07 2009 +0200
     1.3 @@ -441,8 +441,8 @@
     1.4  fun synchronize_inst_syntax ctxt =
     1.5    let
     1.6      val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
     1.7 -    val thy = ProofContext.theory_of ctxt;
     1.8 -    fun subst (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
     1.9 +    val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of (ProofContext.theory_of ctxt));
    1.10 +    fun subst (c, ty) = case inst_tyco_of (c, ty)
    1.11           of SOME tyco => (case AList.lookup (op =) params (c, tyco)
    1.12               of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
    1.13                | NONE => NONE)
    1.14 @@ -512,9 +512,11 @@
    1.15      fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
    1.16       of NONE => NONE
    1.17        | SOME ts' => SOME (ts', ctxt);
    1.18 -    fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
    1.19 +    val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of thy);
    1.20 +    val typ_instance = Type.typ_instance (Sign.tsig_of thy);
    1.21 +    fun improve (c, ty) = case inst_tyco_of (c, ty)
    1.22       of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
    1.23 -         of SOME (_, ty') => if Type.typ_instance (Sign.tsig_of thy) (ty', ty)
    1.24 +         of SOME (_, ty') => if typ_instance (ty', ty)
    1.25                then SOME (ty, ty') else NONE
    1.26            | NONE => NONE)
    1.27        | NONE => NONE;
     2.1 --- a/src/Pure/axclass.ML	Wed May 20 10:37:38 2009 +0200
     2.2 +++ b/src/Pure/axclass.ML	Wed May 20 12:09:07 2009 +0200
     2.3 @@ -26,9 +26,9 @@
     2.4    val axiomatize_arity: arity -> theory -> theory
     2.5    val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
     2.6    val instance_name: string * class -> string
     2.7 +  val inst_tyco_of: Consts.T -> string * typ -> string option
     2.8    val declare_overloaded: string * typ -> theory -> term * theory
     2.9    val define_overloaded: binding -> string * term -> theory -> thm * theory
    2.10 -  val inst_tyco_of: theory -> string * typ -> string option
    2.11    val unoverload: theory -> thm -> thm
    2.12    val overload: theory -> thm -> thm
    2.13    val unoverload_conv: theory -> conv
    2.14 @@ -249,7 +249,8 @@
    2.15  fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
    2.16    (get_inst_params thy) [];
    2.17  
    2.18 -fun inst_tyco_of thy = try (fst o dest_Type o the_single o Sign.const_typargs thy);
    2.19 +fun inst_tyco_of consts = try (fst o dest_Type o the_single o Consts.typargs consts);
    2.20 +val inst_tyco_of' = inst_tyco_of o Sign.consts_of;
    2.21  
    2.22  fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
    2.23  fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
    2.24 @@ -259,7 +260,7 @@
    2.25  
    2.26  fun unoverload_const thy (c_ty as (c, _)) =
    2.27    case class_of_param thy c
    2.28 -   of SOME class => (case inst_tyco_of thy c_ty
    2.29 +   of SOME class => (case inst_tyco_of' thy c_ty
    2.30         of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
    2.31          | NONE => c)
    2.32      | NONE => c;
    2.33 @@ -293,7 +294,7 @@
    2.34      val class = case class_of_param thy c
    2.35       of SOME class => class
    2.36        | NONE => error ("Not a class parameter: " ^ quote c);
    2.37 -    val tyco = case inst_tyco_of thy (c, T)
    2.38 +    val tyco = case inst_tyco_of' thy (c, T)
    2.39       of SOME tyco => tyco
    2.40        | NONE => error ("Illegal type for instantiation of class parameter: "
    2.41          ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
    2.42 @@ -318,7 +319,7 @@
    2.43  fun define_overloaded b (c, t) thy =
    2.44    let
    2.45      val T = Term.fastype_of t;
    2.46 -    val SOME tyco = inst_tyco_of thy (c, T);
    2.47 +    val SOME tyco = inst_tyco_of' thy (c, T);
    2.48      val (c', eq) = get_inst_param thy (c, tyco);
    2.49      val prop = Logic.mk_equals (Const (c', T), t);
    2.50      val b' = Thm.def_binding_optional