remove needless variables
authorblanchet
Fri Jun 11 16:34:56 2010 +0200 (2010-06-11)
changeset 3739618a1e9c7acb0
parent 37394 92a75e6d938b
child 37397 18000f9d783e
remove needless variables
src/HOL/Tools/Nitpick/minipick.ML
src/HOL/Tools/Nitpick/nitpick_tests.ML
     1.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Thu Jun 10 12:28:27 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Fri Jun 11 16:34:56 2010 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4  
     1.5  fun kodkod_formula_from_term ctxt card frees =
     1.6    let
     1.7 -    fun R_rep_from_S_rep (T as Type (@{type_name fun}, [T1, @{typ bool}])) r =
     1.8 +    fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
     1.9          let
    1.10            val jss = atom_schema_of SRep card T1 |> map (rpair 0)
    1.11                      |> all_combinations
    1.12 @@ -115,7 +115,7 @@
    1.13           @{const Not} $ t1 => Not (to_F Ts t1)
    1.14         | @{const False} => False
    1.15         | @{const True} => True
    1.16 -       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
    1.17 +       | Const (@{const_name All}, _) $ Abs (_, T, t') =>
    1.18           All (decls_for SRep card Ts T, to_F (T :: Ts) t')
    1.19         | (t0 as Const (@{const_name All}, _)) $ t1 =>
    1.20           to_F Ts (t0 $ eta_expand Ts t1 1)
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Thu Jun 10 12:28:27 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Fri Jun 11 16:34:56 2010 +0200
     2.3 @@ -298,7 +298,6 @@
     2.4      val peephole_optim = true
     2.5      val nat_card = 4
     2.6      val int_card = 9
     2.7 -    val bits = 8
     2.8      val j0 = 0
     2.9      val constrs = kodkod_constrs peephole_optim nat_card int_card j0
    2.10      val (free_rels, pool, table) =