# HG changeset patch
# User bulwahn
# Date 1258615554 -3600
# Node ID 6dc1b67f2127bc50231dd82d285c7ccd57c68f37
# Parent  f2957bd46fafee16e07b0b406ddaeb6561987a03
concealing internal definitions of primrec specifications

diff -r f2957bd46faf -r 6dc1b67f2127 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Thu Nov 19 08:25:53 2009 +0100
+++ b/src/HOL/Tools/primrec.ML	Thu Nov 19 08:25:54 2009 +0100
@@ -198,7 +198,7 @@
       (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
     val rhs = singleton (Syntax.check_terms ctxt)
       (TypeInfer.constrain varT raw_rhs);
-  in (var, ((Binding.name def_name, []), rhs)) end;
+  in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end;
 
 
 (* find datatypes which contain all datatypes in tnames' *)