# 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);