removed dead code
authorblanchet
Wed Oct 07 15:31:47 2015 +0200 (2015-10-07)
changeset 6135725ca76cfa9ce
parent 61356 1c710116b44d
child 61358 131fc8c10402
removed dead code
src/HOL/Tools/Nitpick/nitpick_model.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Oct 07 13:53:54 2015 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Oct 07 15:31:47 2015 +0200
     1.3 @@ -151,12 +151,8 @@
     1.4      | _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
     1.5    end
     1.6  
     1.7 -fun nth_atom thy atomss pool for_auto T j =
     1.8 -  if for_auto then
     1.9 -    Free (nth_atom_name thy atomss pool (hd (Long_Name.explode nitpick_prefix))
    1.10 -                        T j, T)
    1.11 -  else
    1.12 -    Const (nth_atom_name thy atomss pool "" T j, T)
    1.13 +fun nth_atom thy atomss pool T j =
    1.14 +  Const (nth_atom_name thy atomss pool "" T j, T)
    1.15  
    1.16  fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
    1.17      real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
    1.18 @@ -375,7 +371,6 @@
    1.19                     data_types, ofs, ...})
    1.20          atomss sel_names rel_table bounds =
    1.21    let
    1.22 -    val for_auto = (maybe_name = "")
    1.23      fun value_of_bits jss =
    1.24        let
    1.25          val j0 = offset_of_type ofs @{typ unsigned_bit}
    1.26 @@ -530,15 +525,14 @@
    1.27          else if T = @{typ bisim_iterator} then
    1.28            HOLogic.mk_number nat_T j
    1.29          else case data_type_spec data_types T of
    1.30 -          NONE => nth_atom thy atomss pool for_auto T j
    1.31 -        | SOME {deep = false, ...} => nth_atom thy atomss pool for_auto T j
    1.32 +          NONE => nth_atom thy atomss pool T j
    1.33 +        | SOME {deep = false, ...} => nth_atom thy atomss pool T j
    1.34          | SOME {co, constrs, ...} =>
    1.35            let
    1.36              fun tuples_for_const (s, T) =
    1.37                tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
    1.38              fun cyclic_atom () =
    1.39 -              nth_atom thy atomss pool for_auto (Type (cyclic_type_name (), []))
    1.40 -                       j
    1.41 +              nth_atom thy atomss pool (Type (cyclic_type_name (), [])) j
    1.42              fun cyclic_var () =
    1.43                Var ((nth_atom_name thy atomss pool "" T j, 0), T)
    1.44              val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
    1.45 @@ -593,9 +587,8 @@
    1.46                        frac_from_term_pair (body_type T) t1 t2
    1.47                      | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
    1.48                                         \term_for_atom (Abs_Frac)", ts)
    1.49 -                  else if not for_auto andalso
    1.50 -                          (is_abs_fun ctxt constr_x orelse
    1.51 -                           constr_s = @{const_name Quot}) then
    1.52 +                  else if is_abs_fun ctxt constr_x orelse
    1.53 +                          constr_s = @{const_name Quot} then
    1.54                      Const (abs_name, constr_T) $ the_single ts
    1.55                    else
    1.56                      list_comb (Const constr_x, ts)