src/Pure/axclass.ML
changeset 36610 bafd82950e24
parent 36456 9fd0f1eacd35
child 36740 6248aa22c694
     1.1 --- a/src/Pure/axclass.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -198,7 +198,7 @@
     1.4    (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
     1.5      SOME thm => Thm.transfer thy thm
     1.6    | NONE => error ("Unproven class relation " ^
     1.7 -      Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
     1.8 +      Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2]));
     1.9  
    1.10  fun put_trancl_classrel ((c1, c2), th) thy =
    1.11    let
    1.12 @@ -245,7 +245,7 @@
    1.13    (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
    1.14      SOME (thm, _) => Thm.transfer thy thm
    1.15    | NONE => error ("Unproven type arity " ^
    1.16 -      Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
    1.17 +      Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c])));
    1.18  
    1.19  fun thynames_of_arity thy (c, a) =
    1.20    Symtab.lookup_list (proven_arities_of thy) a
    1.21 @@ -357,7 +357,7 @@
    1.22    in (c1, c2) end;
    1.23  
    1.24  fun read_classrel thy raw_rel =
    1.25 -  cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel)
    1.26 +  cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init_global thy)) raw_rel)
    1.27      handle TYPE (msg, _, _) => error msg;
    1.28  
    1.29  
    1.30 @@ -461,7 +461,7 @@
    1.31  
    1.32  fun prove_classrel raw_rel tac thy =
    1.33    let
    1.34 -    val ctxt = ProofContext.init thy;
    1.35 +    val ctxt = ProofContext.init_global thy;
    1.36      val (c1, c2) = cert_classrel thy raw_rel;
    1.37      val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
    1.38        cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
    1.39 @@ -475,7 +475,7 @@
    1.40  
    1.41  fun prove_arity raw_arity tac thy =
    1.42    let
    1.43 -    val ctxt = ProofContext.init thy;
    1.44 +    val ctxt = ProofContext.init_global thy;
    1.45      val arity = ProofContext.cert_arity ctxt raw_arity;
    1.46      val names = map (prefix arity_prefix) (Logic.name_arities arity);
    1.47      val props = Logic.mk_arities arity;
    1.48 @@ -509,7 +509,7 @@
    1.49  
    1.50  fun define_class (bclass, raw_super) raw_params raw_specs thy =
    1.51    let
    1.52 -    val ctxt = ProofContext.init thy;
    1.53 +    val ctxt = ProofContext.init_global thy;
    1.54      val pp = Syntax.pp ctxt;
    1.55  
    1.56  
    1.57 @@ -623,7 +623,7 @@
    1.58      (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
    1.59  
    1.60  fun ax_arity prep =
    1.61 -  axiomatize (prep o ProofContext.init) Logic.mk_arities
    1.62 +  axiomatize (prep o ProofContext.init_global) Logic.mk_arities
    1.63      (map (prefix arity_prefix) o Logic.name_arities) add_arity;
    1.64  
    1.65  fun class_const c =
    1.66 @@ -643,7 +643,7 @@
    1.67  in
    1.68  
    1.69  val axiomatize_class = ax_class Sign.certify_class cert_classrel;
    1.70 -val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init) read_classrel;
    1.71 +val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init_global) read_classrel;
    1.72  val axiomatize_classrel = ax_classrel cert_classrel;
    1.73  val axiomatize_classrel_cmd = ax_classrel read_classrel;
    1.74  val axiomatize_arity = ax_arity ProofContext.cert_arity;