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