src/Pure/Isar/rule_cases.ML
changeset 35625 9c818cab0dd0
parent 35408 b48ab741683b
child 36354 bbd742107f56
     1.1 --- a/src/Pure/Isar/rule_cases.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/Pure/Isar/rule_cases.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -110,7 +110,7 @@
     1.4          val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) case_outline prop
     1.5            |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
     1.6  
     1.7 -        val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop);
     1.8 +        val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
     1.9          val binds =
    1.10            (case_conclN, concl) :: dest_binops concls concl
    1.11            |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));