# HG changeset patch
# User wenzelm
# Date 878564255 -3600
# Node ID 9f6907c40442f46060ae77585a3190698599876a
# Parent  0ec0d2dbe3f4cbc6c6251a011dcde5bc007acd08
isatool fixclasimp;

diff -r 0ec0d2dbe3f4 -r 9f6907c40442 src/HOL/ex/Recdef.thy
--- a/src/HOL/ex/Recdef.thy	Mon Nov 03 14:09:16 1997 +0100
+++ b/src/HOL/ex/Recdef.thy	Mon Nov 03 14:37:35 1997 +0100
@@ -31,7 +31,7 @@
 
 consts qsort   ::"('a => 'a => bool) * 'a list => 'a list"
 recdef qsort "measure (size o snd)"
-    simpset "!simpset addsimps [le_eq_less_Suc RS sym, filter_size]"
+    simpset "simpset() addsimps [le_eq_less_Suc RS sym, filter_size]"
     "qsort(ord, [])    = []"
     "qsort(ord, x#rst) = qsort(ord, filter(Not o ord x) rst)  
                          @ [x] @   
@@ -44,7 +44,7 @@
 
 consts gcd :: "nat * nat => nat"
 recdef gcd "measure (%(x,y).x+y)"
-    simpset "!simpset addsimps [le_eq_less_Suc RS sym, le_add1, diff_le_self]"
+    simpset "simpset() addsimps [le_eq_less_Suc RS sym, le_add1, diff_le_self]"
     "gcd (0,y)          = y"
     "gcd (Suc x, 0)     = Suc x"
     "gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y)