--- 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;