src/Provers/splitter.ML
changeset 35625 9c818cab0dd0
parent 33955 fff6f11b1f09
child 42364 8c674b3b8e44
     1.1 --- a/src/Provers/splitter.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/Provers/splitter.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -46,14 +46,14 @@
     1.4  struct
     1.5  
     1.6  val Const (const_not, _) $ _ =
     1.7 -  ObjectLogic.drop_judgment Data.thy
     1.8 +  Object_Logic.drop_judgment Data.thy
     1.9      (#1 (Logic.dest_implies (Thm.prop_of Data.notnotD)));
    1.10  
    1.11  val Const (const_or , _) $ _ $ _ =
    1.12 -  ObjectLogic.drop_judgment Data.thy
    1.13 +  Object_Logic.drop_judgment Data.thy
    1.14      (#1 (Logic.dest_implies (Thm.prop_of Data.disjE)));
    1.15  
    1.16 -val const_Trueprop = ObjectLogic.judgment_name Data.thy;
    1.17 +val const_Trueprop = Object_Logic.judgment_name Data.thy;
    1.18  
    1.19  
    1.20  fun split_format_err () = error "Wrong format for split rule";