src/Pure/axclass.ML
changeset 59859 f9d1442c70f3
parent 59621 291934bac95e
child 60801 7664e0916eec
     1.1 --- a/src/Pure/axclass.ML	Mon Mar 30 22:34:59 2015 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Mar 31 00:11:54 2015 +0200
     1.3 @@ -362,7 +362,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 -        #> Global_Theory.add_thm ((Binding.conceal (Binding.name c'), thm), [])
     1.8 +        #> Global_Theory.add_thm ((Binding.concealed (Binding.name c'), thm), [])
     1.9          #> #2
    1.10          #> pair (Const (c, T))))
    1.11      ||> Sign.restore_naming thy
    1.12 @@ -392,7 +392,7 @@
    1.13      val rel = Logic.dest_classrel prop handle TERM _ => err ();
    1.14      val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
    1.15      val binding =
    1.16 -      Binding.conceal (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))));
    1.17 +      Binding.concealed (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))));
    1.18      val (th', thy') = Global_Theory.store_thm (binding, th) thy;
    1.19      val th'' = th'
    1.20        |> Thm.unconstrainT
    1.21 @@ -413,7 +413,7 @@
    1.22      val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
    1.23  
    1.24      val binding =
    1.25 -      Binding.conceal (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
    1.26 +      Binding.concealed (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
    1.27      val (th', thy') = Global_Theory.store_thm (binding, th) thy;
    1.28  
    1.29      val args = Name.invent_names Name.context Name.aT Ss;