src/Pure/axclass.ML
changeset 42375 774df7c59508
parent 42360 da8817d01e7c
child 42383 0ae4ad40d7b5
     1.1 --- a/src/Pure/axclass.ML	Sun Apr 17 13:47:22 2011 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sun Apr 17 19:54:04 2011 +0200
     1.3 @@ -384,9 +384,9 @@
     1.4    in
     1.5      thy
     1.6      |> Sign.qualified_path true (Binding.name name_inst)
     1.7 -    |> Sign.declare_const ((Binding.name c', T'), NoSyn)
     1.8 +    |> Sign.declare_const_global ((Binding.name c', T'), NoSyn)
     1.9      |-> (fn const' as Const (c'', _) =>
    1.10 -      Thm.add_def false true
    1.11 +      Thm.add_def_global false true
    1.12          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
    1.13        #>> apsnd Thm.varifyT_global
    1.14        #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
    1.15 @@ -405,7 +405,7 @@
    1.16      val b' = Thm.def_binding_optional (Binding.name (instance_name (tyco, c))) b;
    1.17    in
    1.18      thy
    1.19 -    |> Thm.add_def false false (b', prop)
    1.20 +    |> Thm.add_def_global false false (b', prop)
    1.21      |>> (fn (_, thm) => Drule.transitive_thm OF [eq, thm])
    1.22    end;
    1.23  
    1.24 @@ -608,7 +608,7 @@
    1.25      val names = name args;
    1.26    in
    1.27      thy
    1.28 -    |> fold_map Thm.add_axiom (map Binding.name names ~~ specs)
    1.29 +    |> fold_map Thm.add_axiom_global (map Binding.name names ~~ specs)
    1.30      |-> fold (add o Drule.export_without_context o snd)
    1.31    end;
    1.32  
    1.33 @@ -631,13 +631,14 @@
    1.34      thy
    1.35      |> Sign.primitive_class (bclass, super)
    1.36      |> ax_classrel prep_classrel (map (fn c => (class, c)) super)
    1.37 -    |> Theory.add_deps "" (class_const class) (map class_const super)
    1.38 +    |> Theory.add_deps_global "" (class_const class) (map class_const super)
    1.39    end;
    1.40  
    1.41  in
    1.42  
    1.43  val axiomatize_class = ax_class Sign.certify_class cert_classrel;
    1.44 -val axiomatize_class_cmd = ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel;
    1.45 +val axiomatize_class_cmd =
    1.46 +  ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel;
    1.47  val axiomatize_classrel = ax_classrel cert_classrel;
    1.48  val axiomatize_classrel_cmd = ax_classrel read_classrel;
    1.49  val axiomatize_arity = ax_arity Proof_Context.cert_arity;