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";
 *)