src/Pure/axclass.ML
changeset 42360 da8817d01e7c
parent 41228 e1fce873b814
child 42375 774df7c59508
     1.1 --- a/src/Pure/axclass.ML	Sat Apr 16 15:25:25 2011 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sat Apr 16 15:47:52 2011 +0200
     1.3 @@ -198,7 +198,7 @@
     1.4    (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
     1.5      SOME thm => thm
     1.6    | NONE => error ("Unproven class relation " ^
     1.7 -      Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2]));  (* FIXME stale thy (!?) *)
     1.8 +      Syntax.string_of_classrel (Proof_Context.init_global thy) [c1, c2]));  (* FIXME stale thy (!?) *)
     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
    1.15    | NONE => error ("Unproven type arity " ^
    1.16 -      Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c])));  (* FIXME stale thy (!?) *)
    1.17 +      Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c])));  (* FIXME stale thy (!?) *)
    1.18  
    1.19  fun thynames_of_arity thy (c, a) =
    1.20    Symtab.lookup_list (proven_arities_of thy) a
    1.21 @@ -359,7 +359,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_global thy)) raw_rel)
    1.26 +  cert_classrel thy (pairself (Proof_Context.read_class (Proof_Context.init_global thy)) raw_rel)
    1.27      handle TYPE (msg, _, _) => error msg;
    1.28  
    1.29  
    1.30 @@ -464,7 +464,7 @@
    1.31  
    1.32  fun prove_classrel raw_rel tac thy =
    1.33    let
    1.34 -    val ctxt = ProofContext.init_global thy;
    1.35 +    val ctxt = Proof_Context.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,8 +475,8 @@
    1.40  
    1.41  fun prove_arity raw_arity tac thy =
    1.42    let
    1.43 -    val ctxt = ProofContext.init_global thy;
    1.44 -    val arity = ProofContext.cert_arity ctxt raw_arity;
    1.45 +    val ctxt = Proof_Context.init_global thy;
    1.46 +    val arity = Proof_Context.cert_arity ctxt raw_arity;
    1.47      val names = map (prefix arity_prefix) (Logic.name_arities arity);
    1.48      val props = Logic.mk_arities arity;
    1.49      val ths = Goal.prove_multi ctxt [] [] props
    1.50 @@ -617,7 +617,7 @@
    1.51      (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
    1.52  
    1.53  fun ax_arity prep =
    1.54 -  axiomatize (prep o ProofContext.init_global) Logic.mk_arities
    1.55 +  axiomatize (prep o Proof_Context.init_global) Logic.mk_arities
    1.56      (map (prefix arity_prefix) o Logic.name_arities) add_arity;
    1.57  
    1.58  fun class_const c =
    1.59 @@ -637,11 +637,11 @@
    1.60  in
    1.61  
    1.62  val axiomatize_class = ax_class Sign.certify_class cert_classrel;
    1.63 -val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init_global) read_classrel;
    1.64 +val axiomatize_class_cmd = ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel;
    1.65  val axiomatize_classrel = ax_classrel cert_classrel;
    1.66  val axiomatize_classrel_cmd = ax_classrel read_classrel;
    1.67 -val axiomatize_arity = ax_arity ProofContext.cert_arity;
    1.68 -val axiomatize_arity_cmd = ax_arity ProofContext.read_arity;
    1.69 +val axiomatize_arity = ax_arity Proof_Context.cert_arity;
    1.70 +val axiomatize_arity_cmd = ax_arity Proof_Context.read_arity;
    1.71  
    1.72  end;
    1.73