author | bulwahn |
Thu, 19 Nov 2009 08:25:54 +0100 | |
changeset 33755 | 6dc1b67f2127 |
parent 33754 | f2957bd46faf |
child 33756 | 47b7c9e0bf6e |
--- 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' *)