src/HOL/Tools/SMT2/z3_new_proof.ML
changeset 56245 84fc7dfa3cd4
parent 56122 40f7b45b2472
child 56811 b66639331db5
     1.1 --- a/src/HOL/Tools/SMT2/z3_new_proof.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT2/z3_new_proof.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -463,7 +463,7 @@
     1.4      val match = Sign.typ_match (Proof_Context.theory_of ctxt)
     1.5  
     1.6      val t' = singleton (Variable.polymorphic ctxt) t
     1.7 -    val patTs = map snd (Term.strip_qnt_vars @{const_name all} t')
     1.8 +    val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t')
     1.9      val objTs = map (the o Symtab.lookup env) bounds
    1.10      val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty)
    1.11    in Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end
    1.12 @@ -501,7 +501,7 @@
    1.13      SOME (tyenv, _) => subst_of tyenv
    1.14    | NONE => strip_match ctxt pat (i + 1) (dest_quant i obj))
    1.15  
    1.16 -fun dest_all i (Const (@{const_name all}, _) $ (a as Abs (_, T, _))) =
    1.17 +fun dest_all i (Const (@{const_name Pure.all}, _) $ (a as Abs (_, T, _))) =
    1.18        dest_all (i + 1) (Term.betapply (a, Var (("", i), T)))
    1.19    | dest_all i t = (i, t)
    1.20  
    1.21 @@ -517,7 +517,7 @@
    1.22      | SOME subst =>
    1.23          let
    1.24            val applyT = Same.commit (substTs_same subst)
    1.25 -          val patTs = map snd (Term.strip_qnt_vars @{const_name all} t'')
    1.26 +          val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t'')
    1.27          in SOME (Symtab.make (bs' ~~ map applyT patTs)) end)
    1.28    end
    1.29