src/HOL/thy_syntax.ML
changeset 4091 771b1f6422a8
parent 4032 4b1c69d8b767
child 4106 01fa6e7e7196
     1.1 --- a/src/HOL/thy_syntax.ML	Mon Nov 03 12:22:43 1997 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Mon Nov 03 12:24:13 1997 +0100
     1.3 @@ -276,7 +276,7 @@
     1.4  
     1.5  val rec_decl = (name -- string -- 
     1.6  		optional ("congs" $$-- string >> trim) "[]" -- 
     1.7 -		optional ("simpset" $$-- string >> trim) "!simpset" -- 
     1.8 +		optional ("simpset" $$-- string >> trim) "simpset()" -- 
     1.9  		repeat1 string >> mk_rec_decl) ;
    1.10  
    1.11