tuned goal conversion interfaces;
authorwenzelm
Thu Jul 05 00:06:23 2007 +0200 (2007-07-05)
changeset 235849b5ba76de1c2
parent 23583 00751df1f98c
child 23585 f07ef41ffb87
tuned goal conversion interfaces;
src/Pure/Isar/rule_cases.ML
src/Pure/meta_simplifier.ML
src/Pure/tctical.ML
     1.1 --- a/src/Pure/Isar/rule_cases.ML	Thu Jul 05 00:06:22 2007 +0200
     1.2 +++ b/src/Pure/Isar/rule_cases.ML	Thu Jul 05 00:06:23 2007 +0200
     1.3 @@ -189,14 +189,14 @@
     1.4  
     1.5  fun unfold_prems n defs th =
     1.6    if null defs then th
     1.7 -  else Conv.fconv_rule (Conv.prems_conv n (K (MetaSimplifier.rewrite true defs))) th;
     1.8 +  else Conv.fconv_rule (Conv.prems_conv n (MetaSimplifier.rewrite true defs)) th;
     1.9  
    1.10  fun unfold_prems_concls defs th =
    1.11    if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
    1.12    else
    1.13      Conv.fconv_rule
    1.14        (Conv.concl_conv ~1 (Conjunction.convs
    1.15 -        (Conv.prems_conv ~1 (K (MetaSimplifier.rewrite true defs))))) th;
    1.16 +        (Conv.prems_conv ~1 (MetaSimplifier.rewrite true defs)))) th;
    1.17  
    1.18  in
    1.19  
     2.1 --- a/src/Pure/meta_simplifier.ML	Thu Jul 05 00:06:22 2007 +0200
     2.2 +++ b/src/Pure/meta_simplifier.ML	Thu Jul 05 00:06:23 2007 +0200
     2.3 @@ -1271,13 +1271,13 @@
     2.4  
     2.5  (*Rewrite the subgoals of a proof state (represented by a theorem)*)
     2.6  fun rewrite_goals_rule thms th =
     2.7 -  Conv.fconv_rule (Conv.prems_conv ~1 (K (rewrite_cterm (true, true, true) simple_prover
     2.8 -    (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms)))) th;
     2.9 +  Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
    2.10 +    (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
    2.11  
    2.12  (*Rewrite the subgoal of a proof state (represented by a theorem)*)
    2.13  fun rewrite_goal_rule mode prover ss i thm =
    2.14    if 0 < i andalso i <= Thm.nprems_of thm
    2.15 -  then Conv.goal_conv_rule (rewrite_cterm mode prover ss) i thm
    2.16 +  then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm
    2.17    else raise THM ("rewrite_goal_rule", i, [thm]);
    2.18  
    2.19  
     3.1 --- a/src/Pure/tctical.ML	Thu Jul 05 00:06:22 2007 +0200
     3.2 +++ b/src/Pure/tctical.ML	Thu Jul 05 00:06:23 2007 +0200
     3.3 @@ -522,7 +522,7 @@
     3.4  fun SINGLE tacf = Option.map fst o Seq.pull o tacf
     3.5  
     3.6  (*Conversions as tactics*)
     3.7 -fun CONVERSION cv i st = Seq.single (Conv.goal_conv_rule cv i st)
     3.8 +fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st)
     3.9    handle THM _ => Seq.empty
    3.10      | CTERM _ => Seq.empty
    3.11      | TERM _ => Seq.empty