# HG changeset patch
# User wenzelm
# Date 1452769882 -3600
# Node ID c3c98ed94b0f7c738e65e66f9bdefaced354bae3
# Parent  3a578ee55bffcdebcbd5b2147976aae5688e059e
made SML/NJ happy;

diff -r 3a578ee55bff -r c3c98ed94b0f src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Wed Jan 13 23:37:55 2016 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Thu Jan 14 12:11:22 2016 +0100
@@ -165,7 +165,7 @@
 
 in
 
-val nominal_induct_method =
+val nominal_induct_method : (Proof.context -> Proof.method) context_parser =
   Scan.lift (Args.mode Induct.no_simpN) --
   (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
     avoiding -- fixing -- rule_spec) >>