remove needless variables
authorblanchet
Fri, 11 Jun 2010 16:34:56 +0200
changeset 37396 18a1e9c7acb0
parent 37394 92a75e6d938b
child 37397 18000f9d783e
remove needless variables
src/HOL/Tools/Nitpick/minipick.ML
src/HOL/Tools/Nitpick/nitpick_tests.ML
--- a/src/HOL/Tools/Nitpick/minipick.ML	Thu Jun 10 12:28:27 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Fri Jun 11 16:34:56 2010 +0200
@@ -80,7 +80,7 @@
 
 fun kodkod_formula_from_term ctxt card frees =
   let
-    fun R_rep_from_S_rep (T as Type (@{type_name fun}, [T1, @{typ bool}])) r =
+    fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
         let
           val jss = atom_schema_of SRep card T1 |> map (rpair 0)
                     |> all_combinations
@@ -115,7 +115,7 @@
          @{const Not} $ t1 => Not (to_F Ts t1)
        | @{const False} => False
        | @{const True} => True
-       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
+       | Const (@{const_name All}, _) $ Abs (_, T, t') =>
          All (decls_for SRep card Ts T, to_F (T :: Ts) t')
        | (t0 as Const (@{const_name All}, _)) $ t1 =>
          to_F Ts (t0 $ eta_expand Ts t1 1)
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Thu Jun 10 12:28:27 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Fri Jun 11 16:34:56 2010 +0200
@@ -298,7 +298,6 @@
     val peephole_optim = true
     val nat_card = 4
     val int_card = 9
-    val bits = 8
     val j0 = 0
     val constrs = kodkod_constrs peephole_optim nat_card int_card j0
     val (free_rels, pool, table) =