src/HOL/Tools/TFL/post.ML
changeset 35625 9c818cab0dd0
parent 35365 2fcd08c62495
child 35756 cfde251d03a5
     1.1 --- a/src/HOL/Tools/TFL/post.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/TFL/post.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -151,9 +151,9 @@
     1.4                 {f = f, R = R, rules = rules,
     1.5                  full_pats_TCs = full_pats_TCs,
     1.6                  TCs = TCs}
     1.7 -       val rules' = map (Drule.export_without_context o ObjectLogic.rulify_no_asm)
     1.8 +       val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
     1.9                          (R.CONJUNCTS rules)
    1.10 -         in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
    1.11 +         in  {induct = meta_outer (Object_Logic.rulify_no_asm (induction RS spec')),
    1.12          rules = ListPair.zip(rules', rows),
    1.13          tcs = (termination_goals rules') @ tcs}
    1.14     end
    1.15 @@ -180,7 +180,7 @@
    1.16      | solve_eq (th, [a], i) = [(a, i)]
    1.17      | solve_eq (th, splitths as (_ :: _), i) = 
    1.18        (writeln "Proving unsplit equation...";
    1.19 -      [((Drule.export_without_context o ObjectLogic.rulify_no_asm)
    1.20 +      [((Drule.export_without_context o Object_Logic.rulify_no_asm)
    1.21            (CaseSplit.splitto splitths th), i)])
    1.22        (* if there's an error, pretend nothing happened with this definition 
    1.23           We should probably print something out so that the user knows...? *)