# HG changeset patch
# User nipkow
# Date 1322500087 -3600
# Node ID d32ec2234efc66da7aec1a58b623a11eab61c36c
# Parent  ec6ba4b1f6d58175c6ade8d8b15a693e40ceeca4# Parent  4f7c05990420cb2c2d09f7e96f2bd4c78a8cc6e6
merged

diff -r 4f7c05990420 -r d32ec2234efc src/FOL/simpdata.ML
--- 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 <->");
 
diff -r 4f7c05990420 -r d32ec2234efc src/HOL/Statespace/state_fun.ML
--- 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;
diff -r 4f7c05990420 -r d32ec2234efc src/HOL/Statespace/state_space.ML
--- 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
diff -r 4f7c05990420 -r d32ec2234efc src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- 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"
diff -r 4f7c05990420 -r d32ec2234efc src/Provers/hypsubst.ML
--- 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 #>
diff -r 4f7c05990420 -r d32ec2234efc src/Provers/typedsimp.ML
--- 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) *)
diff -r 4f7c05990420 -r d32ec2234efc src/Sequents/simpdata.ML
--- 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 <->");