src/Pure/axclass.ML
changeset 35669 a91c7ed801b8
parent 35238 18ae6ef02fe0
child 35845 e5980f0ad025
     1.1 --- a/src/Pure/axclass.ML	Tue Mar 09 14:29:47 2010 +0100
     1.2 +++ b/src/Pure/axclass.ML	Tue Mar 09 14:35:02 2010 +0100
     1.3 @@ -280,7 +280,7 @@
     1.4    in (c1, c2) end;
     1.5  
     1.6  fun read_classrel thy raw_rel =
     1.7 -  cert_classrel thy (pairself (Sign.read_class thy) raw_rel)
     1.8 +  cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel)
     1.9      handle TYPE (msg, _, _) => error msg;
    1.10  
    1.11  
    1.12 @@ -387,7 +387,7 @@
    1.13  fun prove_arity raw_arity tac thy =
    1.14    let
    1.15      val ctxt = ProofContext.init thy;
    1.16 -    val arity = Sign.cert_arity thy raw_arity;
    1.17 +    val arity = ProofContext.cert_arity ctxt raw_arity;
    1.18      val names = map (prefix arity_prefix) (Logic.name_arities arity);
    1.19      val props = Logic.mk_arities arity;
    1.20      val ths = Goal.prove_multi ctxt [] [] props
    1.21 @@ -530,7 +530,7 @@
    1.22      (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
    1.23  
    1.24  fun ax_arity prep =
    1.25 -  axiomatize prep Logic.mk_arities
    1.26 +  axiomatize (prep o ProofContext.init) Logic.mk_arities
    1.27      (map (prefix arity_prefix) o Logic.name_arities) add_arity;
    1.28  
    1.29  fun class_const c =
    1.30 @@ -550,11 +550,11 @@
    1.31  in
    1.32  
    1.33  val axiomatize_class = ax_class Sign.certify_class cert_classrel;
    1.34 -val axiomatize_class_cmd = ax_class Sign.read_class read_classrel;
    1.35 +val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init) read_classrel;
    1.36  val axiomatize_classrel = ax_classrel cert_classrel;
    1.37  val axiomatize_classrel_cmd = ax_classrel read_classrel;
    1.38 -val axiomatize_arity = ax_arity Sign.cert_arity;
    1.39 -val axiomatize_arity_cmd = ax_arity Sign.read_arity;
    1.40 +val axiomatize_arity = ax_arity ProofContext.cert_arity;
    1.41 +val axiomatize_arity_cmd = ax_arity ProofContext.read_arity;
    1.42  
    1.43  end;
    1.44