# HG changeset patch
# User haftmann
# Date 1167242998 -3600
# Node ID a6439243512b229971b099ff72e6012e5640df71
# Parent  d02ba728cd565b2c0e630b56b45907bd578d556c
removed Main.thy

diff -r d02ba728cd56 -r a6439243512b src/HOL/Integ/reflected_cooper.ML
--- 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";
 *)
diff -r d02ba728cd56 -r a6439243512b src/HOL/ROOT.ML
--- 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*)
diff -r d02ba728cd56 -r a6439243512b src/HOL/Tools/Presburger/reflected_cooper.ML
--- 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";
 *)