# HG changeset patch
# User haftmann
# Date 1237831275 -3600
# Node ID c98a64746c694ddcb4cfea9d6b8b2dfede0188be
# Parent  4cf38ea4fad2416168c1a5a15f28db569bfb137c
suddenly infix identifier oo occurs in generated code

diff -r 4cf38ea4fad2 -r c98a64746c69 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Mon Mar 23 08:16:24 2009 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Mon Mar 23 19:01:15 2009 +0100
@@ -1995,6 +1995,8 @@
   "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
     (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
 
+code_reserved SML oo
+
 ML {* @{code ferrack_test} () *}
 
 oracle linr_oracle = {*