# HG changeset patch
# User haftmann
# Date 1242814147 -7200
# Node ID d6681ddc046c3413f7448347dbda2034eb6051a1
# Parent  77da3aad591707a61a4e970e0bf2c4647623d505
avoid potential problem with stale theory

diff -r 77da3aad5917 -r d6681ddc046c src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Wed May 20 10:37:38 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Wed May 20 12:09:07 2009 +0200
@@ -441,8 +441,8 @@
 fun synchronize_inst_syntax ctxt =
   let
     val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
-    val thy = ProofContext.theory_of ctxt;
-    fun subst (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
+    val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of (ProofContext.theory_of ctxt));
+    fun subst (c, ty) = case inst_tyco_of (c, ty)
          of SOME tyco => (case AList.lookup (op =) params (c, tyco)
              of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
               | NONE => NONE)
@@ -512,9 +512,11 @@
     fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
      of NONE => NONE
       | SOME ts' => SOME (ts', ctxt);
-    fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
+    val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of thy);
+    val typ_instance = Type.typ_instance (Sign.tsig_of thy);
+    fun improve (c, ty) = case inst_tyco_of (c, ty)
      of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
-         of SOME (_, ty') => if Type.typ_instance (Sign.tsig_of thy) (ty', ty)
+         of SOME (_, ty') => if typ_instance (ty', ty)
               then SOME (ty, ty') else NONE
           | NONE => NONE)
       | NONE => NONE;
diff -r 77da3aad5917 -r d6681ddc046c src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed May 20 10:37:38 2009 +0200
+++ b/src/Pure/axclass.ML	Wed May 20 12:09:07 2009 +0200
@@ -26,9 +26,9 @@
   val axiomatize_arity: arity -> theory -> theory
   val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
   val instance_name: string * class -> string
+  val inst_tyco_of: Consts.T -> string * typ -> string option
   val declare_overloaded: string * typ -> theory -> term * theory
   val define_overloaded: binding -> string * term -> theory -> thm * theory
-  val inst_tyco_of: theory -> string * typ -> string option
   val unoverload: theory -> thm -> thm
   val overload: theory -> thm -> thm
   val unoverload_conv: theory -> conv
@@ -249,7 +249,8 @@
 fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
   (get_inst_params thy) [];
 
-fun inst_tyco_of thy = try (fst o dest_Type o the_single o Sign.const_typargs thy);
+fun inst_tyco_of consts = try (fst o dest_Type o the_single o Consts.typargs consts);
+val inst_tyco_of' = inst_tyco_of o Sign.consts_of;
 
 fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
 fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
@@ -259,7 +260,7 @@
 
 fun unoverload_const thy (c_ty as (c, _)) =
   case class_of_param thy c
-   of SOME class => (case inst_tyco_of thy c_ty
+   of SOME class => (case inst_tyco_of' thy c_ty
        of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
         | NONE => c)
     | NONE => c;
@@ -293,7 +294,7 @@
     val class = case class_of_param thy c
      of SOME class => class
       | NONE => error ("Not a class parameter: " ^ quote c);
-    val tyco = case inst_tyco_of thy (c, T)
+    val tyco = case inst_tyco_of' thy (c, T)
      of SOME tyco => tyco
       | NONE => error ("Illegal type for instantiation of class parameter: "
         ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
@@ -318,7 +319,7 @@
 fun define_overloaded b (c, t) thy =
   let
     val T = Term.fastype_of t;
-    val SOME tyco = inst_tyco_of thy (c, T);
+    val SOME tyco = inst_tyco_of' thy (c, T);
     val (c', eq) = get_inst_param thy (c, tyco);
     val prop = Logic.mk_equals (Const (c', T), t);
     val b' = Thm.def_binding_optional