src/HOL/Tools/Nitpick/minipick.ML
changeset 37396 18a1e9c7acb0
parent 36385 ff5f88702590
child 37678 0040bafffdef
     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)