# HG changeset patch
# User wenzelm
# Date 1322496389 -3600
# Node ID ec6ba4b1f6d58175c6ade8d8b15a693e40ceeca4
# Parent  1d168d6c55c2f7bd7f73a82c4ef75f7e867ddc0e
more antiquotations;

diff -r 1d168d6c55c2 -r ec6ba4b1f6d5 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Mon Nov 28 17:06:20 2011 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Mon Nov 28 17:06:29 2011 +0100
@@ -168,7 +168,7 @@
   Simplifier.simproc_global @{theory} "update_simp" ["update d c n v s"]
     (fn thy => fn ss => fn t =>
       (case t of
-        ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
+        ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s) =>
           let
             val (_ :: _ :: _ :: _ :: sT :: _) = binder_types uT;
               (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*)
@@ -202,7 +202,7 @@
                 * updates again, the optimised term is constructed.
                 *)
             fun mk_updterm already
-                (t as ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s)) =
+                (t as ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s)) =
                   let
                     fun rest already = mk_updterm already;
                     val (dT :: cT :: nT :: vT :: sT :: _) = binder_types uT;