src/HOL/Library/cconv.ML
changeset 60642 48dd1cefb4ae
parent 60054 ef4878146485
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Library/cconv.ML	Fri Jul 03 16:19:45 2015 +0200
     1.2 +++ b/src/HOL/Library/cconv.ML	Sun Jul 05 15:02:30 2015 +0200
     1.3 @@ -182,7 +182,7 @@
     1.4            ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
     1.5        | _ =>  cv ct)
     1.6  
     1.7 -fun inst_imp_cong ct = Thm.instantiate ([], [(@{cpat "?A :: prop"}, ct)]) Drule.imp_cong
     1.8 +fun inst_imp_cong ct = Thm.instantiate ([], [((("A", 0), propT), ct)]) Drule.imp_cong
     1.9  
    1.10  (*rewrite B in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
    1.11  fun concl_cconv 0 cv ct = cv ct
    1.12 @@ -202,10 +202,10 @@
    1.13              NONE => (As, B)
    1.14            | SOME (A,B) => strip_prems (i - 1) (A::As) B
    1.15      val (prem, (prems, concl)) = ct |> Thm.dest_implies ||> strip_prems n [] 
    1.16 -    val rewr_imp_concl = Thm.instantiate ([], [(@{cpat "?C :: prop"}, concl)]) @{thm rewr_imp}
    1.17 +    val rewr_imp_concl = Thm.instantiate ([], [((("C", 0), propT), concl)]) @{thm rewr_imp}
    1.18      val th1 = cv prem RS rewr_imp_concl
    1.19      val nprems = Thm.nprems_of th1
    1.20 -    fun inst_cut_rl ct = Thm.instantiate ([], [(@{cpat "?psi :: prop"}, ct)]) cut_rl
    1.21 +    fun inst_cut_rl ct = Thm.instantiate ([], [((("psi", 0), propT), ct)]) cut_rl
    1.22      fun f p th = (th RS inst_cut_rl p)
    1.23        |> Conv.fconv_rule (Conv.concl_conv nprems (Conv.rewr_conv @{thm imp_cong_eq}))
    1.24    in fold f prems th1 end