src/HOL/Tools/TFL/post.ML
changeset 32957 675c0c7e6a37
parent 32952 aeb1e44fbc19
child 32959 23a8c5ac35f8
     1.1 --- a/src/HOL/Tools/TFL/post.ML	Fri Oct 16 10:55:07 2009 +0200
     1.2 +++ b/src/HOL/Tools/TFL/post.ML	Sat Oct 17 00:52:37 2009 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4  
     1.5  (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
     1.6  val meta_outer =
     1.7 -  curry_rule o standard o
     1.8 +  curry_rule o Drule.standard o
     1.9    rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
    1.10  
    1.11  (*Strip off the outer !P*)
    1.12 @@ -166,7 +166,7 @@
    1.13                 {f = f, R = R, rules = rules,
    1.14                  full_pats_TCs = full_pats_TCs,
    1.15                  TCs = TCs}
    1.16 -       val rules' = map (standard o ObjectLogic.rulify_no_asm)
    1.17 +       val rules' = map (Drule.standard o ObjectLogic.rulify_no_asm)
    1.18                          (R.CONJUNCTS rules)
    1.19           in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
    1.20          rules = ListPair.zip(rules', rows),
    1.21 @@ -195,7 +195,7 @@
    1.22      | solve_eq (th, [a], i) = [(a, i)]
    1.23      | solve_eq (th, splitths as (_ :: _), i) = 
    1.24        (writeln "Proving unsplit equation...";
    1.25 -      [((standard o ObjectLogic.rulify_no_asm)
    1.26 +      [((Drule.standard o ObjectLogic.rulify_no_asm)
    1.27            (CaseSplit.splitto splitths th), i)])
    1.28        (* if there's an error, pretend nothing happened with this definition 
    1.29           We should probably print something out so that the user knows...? *)
    1.30 @@ -252,7 +252,7 @@
    1.31   in (theory,
    1.32       (*return the conjoined induction rule and recursion equations,
    1.33         with assumptions remaining to discharge*)
    1.34 -     standard (induction RS (rules RS conjI)))
    1.35 +     Drule.standard (induction RS (rules RS conjI)))
    1.36   end
    1.37  
    1.38  fun defer thy congs fid seqs =