--- a/src/HOL/Prolog/prolog.ML Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Prolog/prolog.ML Wed Jul 15 23:48:21 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Prolog/prolog.ML
- ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
@@ -60,7 +59,7 @@
in map zero_var_indexes (at thm) end;
val atomize_ss =
- Simplifier.theory_context (the_context ()) empty_ss
+ Simplifier.theory_context @{theory} empty_ss
setmksimps (mksimps mksimps_pairs)
addsimps [
all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)