src/HOL/ex/Lagrange.thy
changeset 26480 544cef16045b
parent 25475 d5a382ccb5cc
child 29667 53103fc8ffa3
--- a/src/HOL/ex/Lagrange.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/ex/Lagrange.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -25,7 +25,7 @@
 
 (* These two simprocs are even less efficient than ordered rewriting
    and kill the second example: *)
-ML_setup {*
+ML {*
   Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
 *}