# HG changeset patch
# User wenzelm
# Date 1380540549 -7200
# Node ID 8b70dba5572ff47ac96336a91afc041b9ce6e316
# Parent  d8f7f3d998de1225dc199f661187036fb7cf7037
tuned whitespace;

diff -r d8f7f3d998de -r 8b70dba5572f src/HOL/Tools/Function/fun_cases.ML
--- a/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 13:20:44 2013 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 13:29:09 2013 +0200
@@ -19,8 +19,9 @@
 
 local
 
-val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
-  (fn _ => assume_tac 1);
+val refl_thin =
+  Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
+    (fn _ => assume_tac 1);
 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
 
@@ -30,25 +31,27 @@
 in
 
 fun mk_fun_cases ctxt prop =
-  let val thy = Proof_Context.theory_of ctxt;
-      fun err () =
-        error (Pretty.string_of (Pretty.block
-          [Pretty.str "Proposition is not a function equation:",
-           Pretty.fbrk, Syntax.pretty_term ctxt prop]));
-      val ((f,_),_) = Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop)
-              handle TERM _ => err ();
-      val info = Function.get_info ctxt f handle List.Empty => err ();
-      val {elims, pelims, is_partial, ...} = info;
-      val elims = if is_partial then pelims else the elims
-      val cprop = cterm_of thy prop;
-      val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
-      fun mk_elim rl =
-        Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
-        |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    fun err () =
+      error (Pretty.string_of (Pretty.block
+        [Pretty.str "Proposition is not a function equation:",
+         Pretty.fbrk, Syntax.pretty_term ctxt prop]));
+    val ((f, _), _) =
+      Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop)
+        handle TERM _ => err ();
+    val info = Function.get_info ctxt f handle List.Empty => err ();
+    val {elims, pelims, is_partial, ...} = info;
+    val elims = if is_partial then pelims else the elims;
+    val cprop = cterm_of thy prop;
+    val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
+    fun mk_elim rl =
+      Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
+      |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
   in
-    case get_first (try mk_elim) (flat elims) of
+    (case get_first (try mk_elim) (flat elims) of
       SOME r => r
-    | NONE => err ()
+    | NONE => err ())
   end;
 
 end;