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' *)