src/HOL/Library/Old_SMT/old_z3_proof_tools.ML
changeset 59621 291934bac95e
parent 59590 7ade9a33c653
child 59634 4b94cc030ba0
     1.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -156,7 +156,7 @@
     1.4      | NONE =>
     1.5          let
     1.6            val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
     1.7 -          val cv = Proof_Context.cterm_of ctxt'
     1.8 +          val cv = Thm.cterm_of ctxt'
     1.9              (Free (n, map Thm.typ_of_cterm cvs' ---> Thm.typ_of_cterm ct))
    1.10            val cu = Drule.list_comb (cv, cvs')
    1.11            val e = (t, (cv, fold_rev Thm.lambda cvs' ct))
    1.12 @@ -229,7 +229,7 @@
    1.13              | _ => fresh_abstraction dcvs ct cx)))
    1.14    in abstr (depth, []) end
    1.15  
    1.16 -val cimp = Thm.cterm_of @{theory} @{const Pure.imp}
    1.17 +val cimp = Thm.global_cterm_of @{theory} @{const Pure.imp}
    1.18  
    1.19  fun deepen depth f x =
    1.20    if depth = 0 then f depth x