suddenly infix identifier oo occurs in generated code
authorhaftmann
Mon Mar 23 19:01:15 2009 +0100 (2009-03-23 ago)
changeset 30684c98a64746c69
parent 30665 4cf38ea4fad2
child 30685 dd5fe091ff04
suddenly infix identifier oo occurs in generated code
src/HOL/Decision_Procs/Ferrack.thy
     1.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Mon Mar 23 08:16:24 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Mon Mar 23 19:01:15 2009 +0100
     1.3 @@ -1995,6 +1995,8 @@
     1.4    "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
     1.5      (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
     1.6  
     1.7 +code_reserved SML oo
     1.8 +
     1.9  ML {* @{code ferrack_test} () *}
    1.10  
    1.11  oracle linr_oracle = {*