src/HOL/Import/shuffler.ML
 changeset 27330 1af2598b5f7d parent 27173 9ae98c3cd3d6 child 27865 27a8ad9612a3
```     1.1 --- a/src/HOL/Import/shuffler.ML	Mon Jun 23 20:00:58 2008 +0200
1.2 +++ b/src/HOL/Import/shuffler.ML	Mon Jun 23 23:45:39 2008 +0200
1.3 @@ -159,13 +159,15 @@
1.4          val cert = cterm_of Pure.thy
1.5          val xT = TFree("'a",[])
1.6          val yT = TFree("'b",[])
1.7 +        val x = Free("x",xT)
1.8 +        val y = Free("y",yT)
1.9          val P = Free("P",xT-->yT-->propT)
1.10 -        val lhs = all xT \$ (Abs("x",xT,all yT \$ (Abs("y",yT,P \$ Bound 1 \$ Bound 0))))
1.11 -        val rhs = all yT \$ (Abs("y",yT,all xT \$ (Abs("x",xT,P \$ Bound 0 \$ Bound 1))))
1.12 +        val lhs = Logic.all x (Logic.all y (P \$ x \$ y))
1.13 +        val rhs = Logic.all y (Logic.all x (P \$ x \$ y))
1.14          val cl = cert lhs
1.15          val cr = cert rhs
1.16 -        val cx = cert (Free("x",xT))
1.17 -        val cy = cert (Free("y",yT))
1.18 +        val cx = cert x
1.19 +        val cy = cert y
1.20          val th1 = assume cr
1.21                           |> forall_elim_list [cy,cx]
1.22                           |> forall_intr_list [cx,cy]
1.23 @@ -415,6 +417,8 @@
1.24  fun mk_free s t = Free (s,t)
1.25  val xT = mk_tfree "a"
1.26  val yT = mk_tfree "b"
1.27 +val x = Free ("x", xT)
1.28 +val y = Free ("y", yT)
1.29  val P  = mk_free "P" (xT-->yT-->propT)
1.30  val Q  = mk_free "Q" (xT-->yT)
1.31  val R  = mk_free "R" (xT-->yT)
1.32 @@ -436,7 +440,7 @@
1.33  fun quant_simproc thy = Simplifier.simproc_i
1.34                             thy
1.35                             "Ordered rewriting of nested quantifiers"
1.36 -                           [all xT \$ (Abs("x",xT,all yT \$ (Abs("y",yT,P \$ Bound 1 \$ Bound 0))))]
1.37 +                           [Logic.all x (Logic.all y (P \$ x \$ y))]
1.38                             quant_rewrite
1.39  fun eta_expand_simproc thy = Simplifier.simproc_i
1.40                           thy
1.41 @@ -446,7 +450,7 @@
1.42  fun eta_contract_simproc thy = Simplifier.simproc_i
1.43                           thy
1.44                           "Smart handling of eta-contractions"
1.45 -                         [all xT \$ (Abs("x",xT,Logic.mk_equals(Q \$ Bound 0,R \$ Bound 0)))]
1.46 +                         [Logic.all x (Logic.mk_equals (Q \$ x, R \$ x))]
1.47                           eta_contract
1.48  end
1.49
1.50 @@ -582,8 +586,7 @@
1.51  fun set_prop thy t =
1.52      let