# HG changeset patch # User haftmann # Date 1272483665 -7200 # Node ID 68a837d1a7542f4fe09cacb7211e049b00a272ef # Parent 353041483b9b97c4a2ce7dbff2eb3989941aa089 modernized structure name diff -r 353041483b9b -r 68a837d1a754 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Wed Apr 28 21:41:05 2010 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Wed Apr 28 21:41:05 2010 +0200 @@ -536,7 +536,7 @@ structure Coopereif = struct -open GeneratedCooper; +open Generated_Cooper; fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s); fun i_of_term vs t = case t