| changeset 28965 | 1de908189869 |
| parent 28335 | 25326092cf9a |
| child 31139 | 0b615ac7eeaf |
--- a/src/HOL/ex/Term_Of_Syntax.thy Wed Dec 03 21:00:39 2008 -0800 +++ b/src/HOL/ex/Term_Of_Syntax.thy Thu Dec 04 14:43:33 2008 +0100 @@ -10,7 +10,7 @@ begin setup {* - Sign.declare_const [] ((Name.binding "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn) + Sign.declare_const [] ((Binding.name "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn) #> snd *}