src/Pure/axclass.ML
changeset 39557 fe5722fce758
parent 39134 917b4b6ba3d2
child 41228 e1fce873b814
     1.1 --- a/src/Pure/axclass.ML	Mon Sep 20 15:29:53 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Mon Sep 20 16:05:25 2010 +0200
     1.3 @@ -390,7 +390,7 @@
     1.4          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
     1.5        #>> apsnd Thm.varifyT_global
     1.6        #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
     1.7 -        #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
     1.8 +        #> Global_Theory.add_thm ((Binding.conceal (Binding.name c'), thm), [])
     1.9          #> #2
    1.10          #> pair (Const (c, T))))
    1.11      ||> Sign.restore_naming thy
    1.12 @@ -419,7 +419,7 @@
    1.13      fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
    1.14      val rel = Logic.dest_classrel prop handle TERM _ => err ();
    1.15      val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
    1.16 -    val (th', thy') = PureThy.store_thm
    1.17 +    val (th', thy') = Global_Theory.store_thm
    1.18        (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
    1.19      val th'' = th'
    1.20        |> Thm.unconstrainT
    1.21 @@ -438,7 +438,7 @@
    1.22      fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
    1.23      val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
    1.24  
    1.25 -    val (th', thy') = PureThy.store_thm
    1.26 +    val (th', thy') = Global_Theory.store_thm
    1.27        (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
    1.28  
    1.29      val args = Name.names Name.context Name.aT Ss;
    1.30 @@ -560,7 +560,7 @@
    1.31      val ([def], def_thy) =
    1.32        thy
    1.33        |> Sign.primitive_class (bclass, super)
    1.34 -      |> PureThy.add_defs false [((Thm.def_binding bconst, class_eq), [])];
    1.35 +      |> Global_Theory.add_defs false [((Thm.def_binding bconst, class_eq), [])];
    1.36      val (raw_intro, (raw_classrel, raw_axioms)) =
    1.37        split_defined (length conjs) def ||> chop (length super);
    1.38  
    1.39 @@ -571,7 +571,7 @@
    1.40      val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
    1.41        def_thy
    1.42        |> Sign.qualified_path true bconst
    1.43 -      |> PureThy.note_thmss ""
    1.44 +      |> Global_Theory.note_thmss ""
    1.45          [((Binding.name "intro", []), [([Drule.export_without_context raw_intro], [])]),
    1.46           ((Binding.name "super", []), [(map Drule.export_without_context raw_classrel, [])]),
    1.47           ((Binding.name "axioms", []),
    1.48 @@ -586,7 +586,8 @@
    1.49        facts_thy
    1.50        |> fold (#2 oo put_trancl_classrel) (map (pair class) super ~~ classrel)
    1.51        |> Sign.qualified_path false bconst
    1.52 -      |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> #2
    1.53 +      |> Global_Theory.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms))
    1.54 +      |> #2
    1.55        |> Sign.restore_naming facts_thy
    1.56        |> map_axclasses (Symtab.update (class, axclass))
    1.57        |> map_params (fold (fn (x, _) => add_param (Syntax.pp ctxt) (x, class)) params);