merged

--- a/src/HOL/Tools/quickcheck_generators.ML	Mon Oct 26 14:54:43 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Mon Oct 26 15:17:02 2009 +0100
@@ -84,7 +84,7 @@
     thy
     |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
     |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
+    |-> (fn eq => Specification.definition (NONE, (apfst (Binding.conceal) Attrib.empty_binding, eq)))
     |> snd
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   end;
@@ -140,7 +140,7 @@
       subst_v (@{term "Suc_code_numeral"} $ t_k) eq];
     val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
     val ((_, eqs2), lthy') = Primrec.add_primrec_simple
-      [((Binding.name random_aux, T), NoSyn)] eqs1 lthy;
+      [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1 lthy;
     val cT_random_aux = inst pt_random_aux;
     val cT_rhs = inst pt_rhs;
     val rule = @{thm random_aux_rec}
@@ -176,7 +176,8 @@
         val projs = mk_proj (aux_lhs) Ts;
         val proj_eqs = map2 (fn v => fn proj => (v, lambda arg proj)) vs projs;
         val proj_defs = map2 (fn Free (name, _) => fn (_, rhs) =>
-          ((Binding.name name, NoSyn), (Attrib.empty_binding, rhs))) vs proj_eqs;
+          ((Binding.conceal (Binding.name name), NoSyn),
+            (apfst (Binding.conceal) Attrib.empty_binding, rhs))) vs proj_eqs;
         val aux_eq' = Pattern.rewrite_term thy proj_eqs [] aux_eq;
         fun prove_eqs aux_simp proj_defs lthy = 
           let
@@ -207,7 +208,8 @@
         val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
         val tac = ALLGOALS (ProofContext.fact_tac ext_simps);
       in (map (fn prop => Skip_Proof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
-    val b = Binding.qualify true prfx (Binding.qualify true name (Binding.name "simps"));
+    val b = Binding.conceal (Binding.qualify true prfx
+      (Binding.qualify true name (Binding.name "simps")));
   in
     lthy
     |> random_aux_primrec_multi (name ^ prfx) proto_eqs
@@ -303,8 +305,8 @@
     |> random_aux_specification prfx random_auxN auxs_eqs
     |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
     |-> (fn random_defs' => fold_map (fn random_def =>
-          Specification.definition (NONE, (Attrib.empty_binding,
-            random_def))) random_defs')
+          Specification.definition (NONE, (apfst (Binding.conceal)
+            Attrib.empty_binding, random_def))) random_defs')
     |> snd
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   end;

--- a/src/Provers/order.ML	Mon Oct 26 14:54:43 2009 +0100
+++ b/src/Provers/order.ML	Mon Oct 26 15:17:02 2009 +0100
@@ -307,7 +307,7 @@
 (*                                                                          *)
 (* ************************************************************************ *)
 
-fun mkasm_partial decomp (less_thms : less_arith) sign (t, n) =
+fun mkasm_partial decomp (less_thms : less_arith) sign (n, t) =
   case decomp sign t of
     SOME (x, rel, y) => (case rel of
       "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
@@ -335,7 +335,7 @@
 (*                                                                          *)
 (* ************************************************************************ *)
 
-fun mkasm_linear decomp (less_thms : less_arith) sign (t, n) =
+fun mkasm_linear decomp (less_thms : less_arith) sign (n, t) =
   case decomp sign t of
     SOME (x, rel, y) => (case rel of
       "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
@@ -1228,7 +1228,7 @@
    val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
    val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
    val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
-   val lesss = flat (ListPair.map (mkasm decomp less_thms thy) (Hs, 0 upto (length Hs - 1)))
+   val lesss = flat (map_index (mkasm decomp less_thms thy) Hs)
    val prfs = gen_solve mkconcl thy (lesss, C);
    val (subgoals, prf) = mkconcl decomp less_thms thy C;
   in

--- a/src/Pure/library.ML	Mon Oct 26 14:54:43 2009 +0100
+++ b/src/Pure/library.ML	Mon Oct 26 15:17:02 2009 +0100
@@ -853,7 +853,7 @@
      of [] => 0
       | [n] => n
       | _ => raise UnequalLengths;
-  in map (fn m => f (map (fn xs => nth xs m) xss)) (0 upto n - 1) end;
+  in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end;