src/Pure/axclass.ML
changeset 24920 2a45e400fdad
parent 24847 bc15dcaed517
child 24929 408becab067e
     1.1 --- a/src/Pure/axclass.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -148,7 +148,8 @@
     1.4  fun the_classrel thy (c1, c2) =
     1.5    (case AList.lookup (op =) (#1 (get_instances thy)) (c1, c2) of
     1.6      SOME th => Thm.transfer thy th
     1.7 -  | NONE => error ("Unproven class relation " ^ Sign.string_of_classrel thy [c1, c2]));
     1.8 +  | NONE => error ("Unproven class relation " ^
     1.9 +      Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
    1.10  
    1.11  fun put_classrel arg = map_instances (fn (classrel, arities) =>
    1.12    (insert (eq_fst op =) arg classrel, arities));
    1.13 @@ -157,7 +158,8 @@
    1.14  fun the_arity thy a (c, Ss) =
    1.15    (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss)  of
    1.16      SOME th => Thm.transfer thy th
    1.17 -  | NONE => error ("Unproven type arity " ^ Sign.string_of_arity thy (a, Ss, [c])));
    1.18 +  | NONE => error ("Unproven type arity " ^
    1.19 +      Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
    1.20  
    1.21  fun put_arity ((t, Ss, c), th) = map_instances (fn (classrel, arities) =>
    1.22    (classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th))));
    1.23 @@ -173,7 +175,7 @@
    1.24      fun pretty_axclass (class, AxClass {def, intro, axioms, params}) =
    1.25        Pretty.block (Pretty.fbreaks
    1.26         [Pretty.block
    1.27 -          [Pretty.str "class ", ProofContext.pretty_sort ctxt [class], Pretty.str ":"],
    1.28 +          [Pretty.str "class ", Syntax.pretty_sort ctxt [class], Pretty.str ":"],
    1.29          Pretty.strs ("parameters:" :: params_of thy class),
    1.30          ProofContext.pretty_fact ctxt ("def", [def]),
    1.31          ProofContext.pretty_fact ctxt (introN, [intro]),
    1.32 @@ -233,11 +235,12 @@
    1.33  
    1.34  fun prove_classrel raw_rel tac thy =
    1.35    let
    1.36 +    val ctxt = ProofContext.init thy;
    1.37      val (c1, c2) = cert_classrel thy raw_rel;
    1.38 -    val th = Goal.prove (ProofContext.init thy) [] []
    1.39 +    val th = Goal.prove ctxt [] []
    1.40          (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg =>
    1.41        cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
    1.42 -        quote (Sign.string_of_classrel thy [c1, c2]));
    1.43 +        quote (Syntax.string_of_classrel ctxt [c1, c2]));
    1.44    in
    1.45      thy
    1.46      |> PureThy.add_thms [((prefix classrel_prefix (Logic.name_classrel (c1, c2)), th), [])]
    1.47 @@ -246,13 +249,14 @@
    1.48  
    1.49  fun prove_arity raw_arity tac thy =
    1.50    let
    1.51 +    val ctxt = ProofContext.init thy;
    1.52      val arity = Sign.cert_arity thy raw_arity;
    1.53      val names = map (prefix arity_prefix) (Logic.name_arities arity);
    1.54      val props = Logic.mk_arities arity;
    1.55 -    val ths = Goal.prove_multi (ProofContext.init thy) [] [] props
    1.56 +    val ths = Goal.prove_multi ctxt [] [] props
    1.57        (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
    1.58          cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
    1.59 -          quote (Sign.string_of_arity thy arity));
    1.60 +          quote (Syntax.string_of_arity ctxt arity));
    1.61    in
    1.62      thy
    1.63      |> PureThy.add_thms (map (rpair []) (names ~~ ths))