changeset 35625 | 9c818cab0dd0 |
parent 33004 | 715566791eb0 |
child 36692 | 54b64d4ad524 |
--- a/src/HOL/Decision_Procs/cooper_tac.ML Sun Mar 07 11:57:16 2010 +0100 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Sun Mar 07 12:19:47 2010 +0100 @@ -66,7 +66,7 @@ fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; -fun linz_tac ctxt q i = ObjectLogic.atomize_prems_tac i THEN (fn st => +fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st => let val g = List.nth (prems_of st, i - 1) val thy = ProofContext.theory_of ctxt