--- a/src/FOL/simpdata.ML Mon Nov 28 11:22:36 2011 +0100
+++ b/src/FOL/simpdata.ML Mon Nov 28 18:08:07 2011 +0100
@@ -27,7 +27,7 @@
(*Congruence rules for = or <-> (instead of ==)*)
fun mk_meta_cong ss rl =
- Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
+ Drule.zero_var_indexes (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
handle THM _ =>
error("Premises and conclusion of congruence rules must use =-equality or <->");
--- a/src/HOL/Statespace/state_fun.ML Mon Nov 28 11:22:36 2011 +0100
+++ b/src/HOL/Statespace/state_fun.ML Mon Nov 28 18:08:07 2011 +0100
@@ -168,7 +168,7 @@
Simplifier.simproc_global @{theory} "update_simp" ["update d c n v s"]
(fn thy => fn ss => fn t =>
(case t of
- ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
+ ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s) =>
let
val (_ :: _ :: _ :: _ :: sT :: _) = binder_types uT;
(*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*)
@@ -202,7 +202,7 @@
* updates again, the optimised term is constructed.
*)
fun mk_updterm already
- (t as ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s)) =
+ (t as ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s)) =
let
fun rest already = mk_updterm already;
val (dT :: cT :: nT :: vT :: sT :: _) = binder_types uT;
--- a/src/HOL/Statespace/state_space.ML Mon Nov 28 11:22:36 2011 +0100
+++ b/src/HOL/Statespace/state_space.ML Mon Nov 28 18:08:07 2011 +0100
@@ -564,7 +564,7 @@
(case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
[] => []
| [_] => []
- | rs => ["Different types for component " ^ n ^": " ^
+ | rs => ["Different types for component " ^ quote n ^ ": " ^
commas (map (Syntax.string_of_typ ctxt o snd) rs)])
val err_dup_types = maps check_type (duplicates fst_eq raw_parent_comps)
@@ -573,7 +573,7 @@
val all_comps = parent_comps @ comps';
val err_comp_in_parent = (case duplicates (op =) (map fst all_comps) of
[] => []
- | xs => ["Components already defined in parents: " ^ commas xs]);
+ | xs => ["Components already defined in parents: " ^ commas_quote xs]);
val errs = err_dup_args @ err_dup_components @ err_extra_frees @
err_dup_types @ err_comp_in_parent;
in if null errs
@@ -611,7 +611,7 @@
if get_silent (Context.Proof ctxt)
then Syntax.const @{const_name StateFun.lookup} $
Syntax.const @{const_syntax undefined} $ Syntax.free n $ s
- else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined", []));
+ else raise TERM ("StateSpace.gen_lookup_tr: component " ^ quote n ^ " not defined", []));
fun lookup_tr ctxt [s, x] =
(case Term_Position.strip_positions x of
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Mon Nov 28 11:22:36 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Mon Nov 28 18:08:07 2011 +0100
@@ -98,7 +98,7 @@
lemma
"list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)"
- quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
+ quickcheck[tester = narrowing, finite_types = false, expect = counterexample, timeout = 60]
oops
lemma "map f xs = F f xs"
--- a/src/Provers/hypsubst.ML Mon Nov 28 11:22:36 2011 +0100
+++ b/src/Provers/hypsubst.ML Mon Nov 28 18:08:07 2011 +0100
@@ -139,7 +139,7 @@
end;
-val ssubst = Drule.export_without_context (Data.sym RS Data.subst);
+val ssubst = Drule.zero_var_indexes (Data.sym RS Data.subst);
fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
case try (Logic.strip_assums_hyp #> hd #>
--- a/src/Provers/typedsimp.ML Mon Nov 28 11:22:36 2011 +0100
+++ b/src/Provers/typedsimp.ML Mon Nov 28 18:08:07 2011 +0100
@@ -43,11 +43,11 @@
(*For simplifying both sides of an equation:
[| a=c; b=c |] ==> b=a
Can use resolve_tac [split_eqn] to prepare an equation for simplification. *)
-val split_eqn = Drule.export_without_context (sym RSN (2,trans) RS sym);
+val split_eqn = Drule.zero_var_indexes (sym RSN (2,trans) RS sym);
(* [| a=b; b=c |] ==> reduce(a,c) *)
-val red_trans = Drule.export_without_context (trans RS red_if_equal);
+val red_trans = Drule.zero_var_indexes (trans RS red_if_equal);
(*For REWRITE rule: Make a reduction rule for simplification, e.g.
[| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *)
--- a/src/Sequents/simpdata.ML Mon Nov 28 11:22:36 2011 +0100
+++ b/src/Sequents/simpdata.ML Mon Nov 28 18:08:07 2011 +0100
@@ -48,7 +48,7 @@
(*Congruence rules for = or <-> (instead of ==)*)
fun mk_meta_cong ss rl =
- Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
+ Drule.zero_var_indexes (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
handle THM _ =>
error("Premises and conclusion of congruence rules must use =-equality or <->");