src/Pure/axclass.ML

--- a/src/Pure/axclass.ML	Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/axclass.ML	Sat Mar 15 03:37:22 2014 +0100
@@ -391,9 +391,9 @@
     fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
     val rel = Logic.dest_classrel prop handle TERM _ => err ();
     val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
-    val (th', thy') =
-      Global_Theory.store_thm
-        (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
+    val binding =
+      Binding.conceal (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))));
+    val (th', thy') = Global_Theory.store_thm (binding, th) thy;
     val th'' = th'
       |> Thm.unconstrainT
       |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
@@ -412,9 +412,9 @@
     fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
     val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
 
-    val (th', thy') =
-      Global_Theory.store_thm
-        (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
+    val binding =
+      Binding.conceal (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
+    val (th', thy') = Global_Theory.store_thm (binding, th) thy;
 
     val args = Name.invent_names Name.context Name.aT Ss;
     val T = Type (t, map TFree args);