src/HOL/Statespace/state_fun.ML
changeset 29064 70a61d58460e
parent 28308 d4396a28fb29
child 29302 eb782d1dc07c
--- a/src/HOL/Statespace/state_fun.ML	Wed Dec 10 06:34:10 2008 -0800
+++ b/src/HOL/Statespace/state_fun.ML	Wed Dec 10 22:55:15 2008 +0100
@@ -49,7 +49,7 @@
 
 in
 val lazy_conj_simproc =
-  Simplifier.simproc HOL.thy "lazy_conj_simp" ["P & Q"]
+  Simplifier.simproc @{theory HOL} "lazy_conj_simp" ["P & Q"]
     (fn thy => fn ss => fn t =>
       (case t of (Const ("op &",_)$P$Q) => 
          let
@@ -273,7 +273,7 @@
      end;
 in
 val ex_lookup_eq_simproc =
-  Simplifier.simproc HOL.thy "ex_lookup_eq_simproc" ["Ex t"]
+  Simplifier.simproc @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
     (fn thy => fn ss => fn t =>
        let
          val ctxt = Simplifier.the_context ss |>