src/Provers/splitter.ML
changeset 28839 32d498cf7595
parent 26711 3a478bfa1650
child 29548 02a52ae34b7a
--- a/src/Provers/splitter.ML	Tue Nov 18 18:25:10 2008 +0100
+++ b/src/Provers/splitter.ML	Tue Nov 18 18:25:42 2008 +0100
@@ -105,7 +105,7 @@
 val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
   [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
   (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
-  (fn {prems = [prem], ...} => rewtac prem THEN rtac reflexive_thm 1)
+  (fn {prems, ...} => rewrite_goals_tac prems THEN rtac reflexive_thm 1)
 
 val trlift = lift RS transitive_thm;
 val _ $ (P $ _) $ _ = concl_of trlift;