--- a/src/HOL/Integ/reflected_cooper.ML Wed Dec 27 19:09:57 2006 +0100
+++ b/src/HOL/Integ/reflected_cooper.ML Wed Dec 27 19:09:58 2006 +0100
@@ -51,7 +51,7 @@
| _ => error "qf_of_term : unknown term!";
(*
-fun parse s = term_of (read_cterm (sign_of Main.thy) (s,HOLogic.boolT));
+fun parse thy s = term_of (Thm.read_cterm thy (s, HOLogic.boolT));
val t = parse "ALL (i::int) (j::int). i < 8* j --> (i - 1 = j + 3 + 2*j) & (j <= -i + k ) | 4 = i | 5 dvd i";
*)
--- a/src/HOL/ROOT.ML Wed Dec 27 19:09:57 2006 +0100
+++ b/src/HOL/ROOT.ML Wed Dec 27 19:09:58 2006 +0100
@@ -37,11 +37,6 @@
with_path "Integ" use_thy "Main";
-structure Main =
-struct
- val thy = theory "Main"
-end;
-
path_add "~~/src/HOL/Library";
Goal "True"; (*leave subgoal package empty*)
--- a/src/HOL/Tools/Presburger/reflected_cooper.ML Wed Dec 27 19:09:57 2006 +0100
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML Wed Dec 27 19:09:58 2006 +0100
@@ -51,7 +51,7 @@
| _ => error "qf_of_term : unknown term!";
(*
-fun parse s = term_of (read_cterm (sign_of Main.thy) (s,HOLogic.boolT));
+fun parse thy s = term_of (Thm.read_cterm thy (s, HOLogic.boolT));
val t = parse "ALL (i::int) (j::int). i < 8* j --> (i - 1 = j + 3 + 2*j) & (j <= -i + k ) | 4 = i | 5 dvd i";
*)