src/Tools/induct.ML
changeset 36960 01594f816e3a
parent 36602 0cbcdfd9e527
child 37523 40c352510065
     1.1 --- a/src/Tools/induct.ML	Mon May 17 15:11:25 2010 +0200
     1.2 +++ b/src/Tools/induct.ML	Mon May 17 23:54:15 2010 +0200
     1.3 @@ -254,8 +254,8 @@
     1.4    end;
     1.5  
     1.6  val _ =
     1.7 -  OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules"
     1.8 -    OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
     1.9 +  Outer_Syntax.improper_command "print_induct_rules" "print induction and cases rules"
    1.10 +    Keyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    1.11        Toplevel.keep (print_rules o Toplevel.context_of)));
    1.12  
    1.13  
    1.14 @@ -845,8 +845,6 @@
    1.15  
    1.16  (** concrete syntax **)
    1.17  
    1.18 -structure P = OuterParse;
    1.19 -
    1.20  val arbitraryN = "arbitrary";
    1.21  val takingN = "taking";
    1.22  val ruleN = "rule";
    1.23 @@ -892,7 +890,7 @@
    1.24      Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
    1.25  
    1.26  val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
    1.27 -  P.and_list1' (Scan.repeat (unless_more_args free))) [];
    1.28 +  Parse.and_list1' (Scan.repeat (unless_more_args free))) [];
    1.29  
    1.30  val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
    1.31    Scan.repeat1 (unless_more_args inst)) [];
    1.32 @@ -902,7 +900,7 @@
    1.33  val cases_setup =
    1.34    Method.setup @{binding cases}
    1.35      (Args.mode no_simpN --
    1.36 -      (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
    1.37 +      (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
    1.38        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
    1.39          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
    1.40            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
    1.41 @@ -910,11 +908,12 @@
    1.42  
    1.43  val induct_setup =
    1.44    Method.setup @{binding induct}
    1.45 -    (Args.mode no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
    1.46 +    (Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
    1.47        (arbitrary -- taking -- Scan.option induct_rule)) >>
    1.48        (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
    1.49          RAW_METHOD_CASES (fn facts =>
    1.50 -          Seq.DETERM (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
    1.51 +          Seq.DETERM
    1.52 +            (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
    1.53      "induction on types or predicates/sets";
    1.54  
    1.55  val coinduct_setup =