# HG changeset patch
# User wenzelm
# Date 1394806342 -3600
# Node ID 27167f903c6d7107370bb5a89a423b25a0f35b45
# Parent  ed2b660a52a1b7baac07ec8606092d2fc3d88926
conceal somewhat obscure internal facts, e.g. relevant for 'print_theorems', 'find_theorems';

diff -r ed2b660a52a1 -r 27167f903c6d src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Mar 14 14:59:43 2014 +0100
+++ b/src/Pure/axclass.ML	Fri Mar 14 15:12: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);