dropped void values
authorhaftmann
Tue Jun 20 08:01:56 2017 +0200 (2017-06-20)
changeset 661325844a096c462
parent 66131 39e1c876bfec
child 66133 0b635a6774fb
dropped void values
src/Pure/Isar/code.ML
     1.1 --- a/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
     1.3 @@ -963,8 +963,8 @@
     1.4    let
     1.5      val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals
     1.6        o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.plain_prop_of) thm;
     1.7 -    val _ = case head of Free _ => true
     1.8 -      | Var _ => true
     1.9 +    val _ = case head of Free _ => ()
    1.10 +      | Var _ => ()
    1.11        | _ => raise TERM ("case_cert", []);
    1.12      val ([(case_var, _)], case_expr) = Term.strip_abs_eta 1 raw_case_expr;
    1.13      val (Const (case_const, _), raw_params) = strip_comb case_expr;