# HG changeset patch
# User haftmann
# Date 1497938516 -7200
# Node ID 5844a096c462544b40779d29b13adc2ef74de9eb
# Parent  39e1c876bfec7943e01149bc2a8c9a6ee30be700
dropped void values

diff -r 39e1c876bfec -r 5844a096c462 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
+++ b/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
@@ -963,8 +963,8 @@
   let
     val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals
       o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.plain_prop_of) thm;
-    val _ = case head of Free _ => true
-      | Var _ => true
+    val _ = case head of Free _ => ()
+      | Var _ => ()
       | _ => raise TERM ("case_cert", []);
     val ([(case_var, _)], case_expr) = Term.strip_abs_eta 1 raw_case_expr;
     val (Const (case_const, _), raw_params) = strip_comb case_expr;