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
```