src/HOL/Tools/inductive_package.ML
changeset 30722 623d4831c8cf
parent 30552 58db56278478
child 31174 f1f1e9b53c81
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Mar 25 21:35:49 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Mar 26 14:14:02 2009 +0100
     1.3 @@ -460,17 +460,18 @@
     1.4  val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
     1.5  
     1.6  
     1.7 -val ind_cases =
     1.8 -  Scan.lift (Scan.repeat1 Args.name_source --
     1.9 -    Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
    1.10 -  (fn (raw_props, fixes) => fn ctxt =>
    1.11 -    let
    1.12 -      val (_, ctxt') = Variable.add_fixes fixes ctxt;
    1.13 -      val props = Syntax.read_props ctxt' raw_props;
    1.14 -      val ctxt'' = fold Variable.declare_term props ctxt';
    1.15 -      val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
    1.16 -    in Method.erule 0 rules end);
    1.17 -
    1.18 +val ind_cases_setup =
    1.19 +  Method.setup @{binding ind_cases}
    1.20 +    (Scan.lift (Scan.repeat1 Args.name_source --
    1.21 +      Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
    1.22 +      (fn (raw_props, fixes) => fn ctxt =>
    1.23 +        let
    1.24 +          val (_, ctxt') = Variable.add_fixes fixes ctxt;
    1.25 +          val props = Syntax.read_props ctxt' raw_props;
    1.26 +          val ctxt'' = fold Variable.declare_term props ctxt';
    1.27 +          val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
    1.28 +        in Method.erule 0 rules end))
    1.29 +    "dynamic case analysis on predicates";
    1.30  
    1.31  
    1.32  (* prove induction rule *)
    1.33 @@ -934,7 +935,7 @@
    1.34  (* setup theory *)
    1.35  
    1.36  val setup =
    1.37 -  Method.setup @{binding ind_cases} ind_cases "dynamic case analysis on predicates" #>
    1.38 +  ind_cases_setup #>
    1.39    Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
    1.40      "declaration of monotonicity rule";
    1.41