# HG changeset patch
# User wenzelm
# Date 1414578809 -3600
# Node ID 4c0ad4162cb799dd32b70d4759aa8575f14284a4
# Parent  625d04d4fd2a1fd83afeff38dc66a442ae456ee4
modernized setup;
tuned whitespace;

diff -r 625d04d4fd2a -r 4c0ad4162cb7 src/HOL/Coinduction.thy
--- a/src/HOL/Coinduction.thy	Wed Oct 29 11:19:27 2014 +0100
+++ b/src/HOL/Coinduction.thy	Wed Oct 29 11:33:29 2014 +0100
@@ -14,6 +14,4 @@
 
 ML_file "Tools/coinduction.ML"
 
-setup Coinduction.setup
-
 end
diff -r 625d04d4fd2a -r 4c0ad4162cb7 src/HOL/Tools/coinduction.ML
--- a/src/HOL/Tools/coinduction.ML	Wed Oct 29 11:19:27 2014 +0100
+++ b/src/HOL/Tools/coinduction.ML	Wed Oct 29 11:33:29 2014 +0100
@@ -9,7 +9,6 @@
 signature COINDUCTION =
 sig
   val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> cases_tactic
-  val setup: theory -> theory
 end;
 
 structure Coinduction : COINDUCTION =
@@ -19,11 +18,12 @@
 open Ctr_Sugar_General_Tactics
 
 fun filter_in_out _ [] = ([], [])
-  | filter_in_out P (x :: xs) = (let
-      val (ins, outs) = filter_in_out P xs;
-    in
-      if P x then (x :: ins, outs) else (ins, x :: outs)
-    end);
+  | filter_in_out P (x :: xs) =
+      let
+        val (ins, outs) = filter_in_out P xs;
+      in
+        if P x then (x :: ins, outs) else (ins, x :: outs)
+      end;
 
 fun ALLGOALS_SKIP skip tac st =
   let fun doall n = if n = skip then all_tac else tac n THEN doall (n - 1)
@@ -43,7 +43,7 @@
 fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
   let
     val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
-    fun find_coinduct t = 
+    fun find_coinduct t =
       Induct.find_coinductP ctxt t @
       (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
     val raw_thm =
@@ -102,7 +102,7 @@
                        val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
                        val inv_thms = init @ [last];
                        val eqs = take e inv_thms;
-                       fun is_local_var t = 
+                       fun is_local_var t =
                          member (fn (t, (_, t')) => t aconv (term_of t')) params t;
                         val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
                         val assms = assms' @ drop e inv_thms
@@ -146,12 +146,13 @@
 
 in
 
-val setup =
-  Method.setup @{binding coinduction}
-    (arbitrary -- Scan.option coinduct_rule >>
-      (fn (arbitrary, opt_rule) => fn ctxt => fn facts =>
-        Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts)))
-    "coinduction on types or predicates/sets";
+val _ =
+  Theory.setup
+    (Method.setup @{binding coinduction}
+      (arbitrary -- Scan.option coinduct_rule >>
+        (fn (arbitrary, opt_rule) => fn ctxt => fn facts =>
+          Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts)))
+      "coinduction on types or predicates/sets");
 
 end;