src/HOL/Import/shuffler.ML
changeset 26424 a6cad32a27b0
parent 26277 461e11226111
child 26662 39483503705f
     1.1 --- a/src/HOL/Import/shuffler.ML	Thu Mar 27 14:41:07 2008 +0100
     1.2 +++ b/src/HOL/Import/shuffler.ML	Thu Mar 27 14:41:09 2008 +0100
     1.3 @@ -90,7 +90,7 @@
     1.4  
     1.5  val weaken =
     1.6      let
     1.7 -        val cert = cterm_of ProtoPure.thy
     1.8 +        val cert = cterm_of Pure.thy
     1.9          val P = Free("P",propT)
    1.10          val Q = Free("Q",propT)
    1.11          val PQ = Logic.mk_implies(P,Q)
    1.12 @@ -109,7 +109,7 @@
    1.13  
    1.14  val imp_comm =
    1.15      let
    1.16 -        val cert = cterm_of ProtoPure.thy
    1.17 +        val cert = cterm_of Pure.thy
    1.18          val P = Free("P",propT)
    1.19          val Q = Free("Q",propT)
    1.20          val R = Free("R",propT)
    1.21 @@ -129,7 +129,7 @@
    1.22  
    1.23  val def_norm =
    1.24      let
    1.25 -        val cert = cterm_of ProtoPure.thy
    1.26 +        val cert = cterm_of Pure.thy
    1.27          val aT = TFree("'a",[])
    1.28          val bT = TFree("'b",[])
    1.29          val v = Free("v",aT)
    1.30 @@ -156,7 +156,7 @@
    1.31  
    1.32  val all_comm =
    1.33      let
    1.34 -        val cert = cterm_of ProtoPure.thy
    1.35 +        val cert = cterm_of Pure.thy
    1.36          val xT = TFree("'a",[])
    1.37          val yT = TFree("'b",[])
    1.38          val P = Free("P",xT-->yT-->propT)
    1.39 @@ -180,7 +180,7 @@
    1.40  
    1.41  val equiv_comm =
    1.42      let
    1.43 -        val cert = cterm_of ProtoPure.thy
    1.44 +        val cert = cterm_of Pure.thy
    1.45          val T    = TFree("'a",[])
    1.46          val t    = Free("t",T)
    1.47          val u    = Free("u",T)