src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 35625 9c818cab0dd0
parent 35416 d8d7d1b785af
child 36348 89c54f51f55a
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -3098,7 +3098,7 @@
     1.4  struct
     1.5  
     1.6  fun frpar_tac T ps ctxt i = 
     1.7 - (ObjectLogic.full_atomize_tac i) 
     1.8 + Object_Logic.full_atomize_tac i
     1.9   THEN (fn st =>
    1.10    let
    1.11      val g = List.nth (cprems_of st, i - 1)
    1.12 @@ -3108,7 +3108,7 @@
    1.13    in rtac (th RS iffD2) i st end);
    1.14  
    1.15  fun frpar2_tac T ps ctxt i = 
    1.16 - (ObjectLogic.full_atomize_tac i) 
    1.17 + Object_Logic.full_atomize_tac i
    1.18   THEN (fn st =>
    1.19    let
    1.20      val g = List.nth (cprems_of st, i - 1)