src/HOL/Record.thy
changeset 36176 3fe7e97ccca8
parent 35146 f7bf73b0d7e5
child 38394 3142c1e21a0e
--- a/src/HOL/Record.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Record.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -455,7 +455,7 @@
 use "Tools/record.ML"
 setup Record.setup
 
-hide (open) const Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
+hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
   iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
   iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
   iso_tuple_update_accessor_eq_assist tuple_iso_tuple