src/HOL/Tools/SMT/smt_normalize.ML
changeset 42361 23f352990944
parent 42190 b6b5846504cd
child 43116 e0add071fa10
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -170,7 +170,7 @@
     1.4      (case Term.strip_comb t of
     1.5        (Const c, ts as _ :: _) =>
     1.6          not (SMT_Builtin.is_builtin_fun_ext ctxt c ts) andalso
     1.7 -        forall (is_constr_pat (ProofContext.theory_of ctxt)) ts
     1.8 +        forall (is_constr_pat (Proof_Context.theory_of ctxt)) ts
     1.9      | _ => false)
    1.10  
    1.11    fun has_all_vars vs t =
    1.12 @@ -218,7 +218,7 @@
    1.13        val (lhs, rhs) = dest_cond_eq ct
    1.14  
    1.15        val vs = map Thm.term_of cvs
    1.16 -      val thy = ProofContext.theory_of ctxt
    1.17 +      val thy = Proof_Context.theory_of ctxt
    1.18  
    1.19        fun get_mpats ct =
    1.20          if is_simp_lhs ctxt (Thm.term_of ct) then minimal_pats vs ct