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 =
```