src/HOL/Decision_Procs/ferrack_tac.ML
changeset 35625 9c818cab0dd0
parent 35233 6af1caf7be69
child 36692 54b64d4ad524
     1.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -73,7 +73,7 @@
     1.4  
     1.5  
     1.6  fun linr_tac ctxt q =
     1.7 -    ObjectLogic.atomize_prems_tac
     1.8 +    Object_Logic.atomize_prems_tac
     1.9          THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
    1.10          THEN' SUBGOAL (fn (g, i) =>
    1.11    let