src/HOL/Library/Old_SMT/old_smt_utils.ML
changeset 59621 291934bac95e
parent 59590 7ade9a33c653
child 59634 4b94cc030ba0
     1.1 --- a/src/HOL/Library/Old_SMT/old_smt_utils.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Library/Old_SMT/old_smt_utils.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -146,7 +146,7 @@
     1.4  (* patterns and instantiations *)
     1.5  
     1.6  fun mk_const_pat thy name destT =
     1.7 -  let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name))
     1.8 +  let val cpat = Thm.global_cterm_of thy (Const (name, Sign.the_const_type thy name))
     1.9    in (destT (Thm.ctyp_of_cterm cpat), cpat) end
    1.10  
    1.11  val destT1 = hd o Thm.dest_ctyp
    1.12 @@ -175,7 +175,7 @@
    1.13  
    1.14  val dest_all_cbinders = repeat_yield (try o dest_cbinder)
    1.15  
    1.16 -val mk_cprop = Thm.apply (Thm.cterm_of @{theory} @{const Trueprop})
    1.17 +val mk_cprop = Thm.apply (Thm.global_cterm_of @{theory} @{const Trueprop})
    1.18  
    1.19  fun dest_cprop ct =
    1.20    (case Thm.term_of ct of