hide (open) const;
authorwenzelm
Mon, 10 Apr 2006 00:34:46 +0200
changeset 19396 0592ea0c68a0
parent 19395 edf92521e8d3
child 19397 524f1cb4652a
hide (open) const;
src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Mon Apr 10 00:33:54 2006 +0200
+++ b/src/HOLCF/Fixrec.thy	Mon Apr 10 00:34:46 2006 +0200
@@ -544,9 +544,6 @@
 
 use "fixrec_package.ML"
 
-setup {*
-  Theory.hide_consts_i false
-    ["Fixrec.return", "Fixrec.bind", "Fixrec.fail"]
-*}
+hide (open) const return bind fail
 
 end