1.1 --- a/test/Pure/Isar/Test_Parse_Isac.thy	Sat Aug 29 12:52:55 2020 +0200
     1.2 +++ b/test/Pure/Isar/Test_Parse_Isac.thy	Sat Aug 29 13:17:01 2020 +0200
     1.3 @@ -734,20 +734,25 @@
     1.4  \<close> 
     1.5  declare [[ML_print_depth = 999]] (* ..for getting complete <Output> *)
     1.6  ML \<open>
     1.7 +body
     1.8 +\<close> ML \<open>
     1.9 +type body = (((((string * string) *
    1.10 +  (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list) *
    1.11 +    ((string * string) * ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list)))) *
    1.12 +        string) * string) * string list)
    1.13 +\<close> ML \<open>
    1.14 +val body_dummy = ((((("", ""),
    1.15 +  ((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []),
    1.16 +    (("", ""), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))),
    1.17 +      ""), ""), [])
    1.18 +\<close> ML \<open>
    1.19 +\<close> ML \<open>
    1.20  val problem =
    1.21    problem_headline --
    1.22 -(**)
    1.23 -    body
    1.24 -(** )
    1.25 -    specification --
    1.26 -    Parse.$$$ "Solution" -- Parse.$$$ ":" --
    1.27 -    (*/----- this will become "and steps".. *)
    1.28 -      (Scan.repeat (
    1.29 -        ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term)  (** ) ||
    1.30 -         (problem >> exec_subproblem)  ( *exec_* make types equal for both args of ||*)
    1.31 -      ))
    1.32 -    (*\----- ..this will become "and steps" *)
    1.33 -( **)
    1.34 +    (Scan.optional
    1.35 +      body
    1.36 +    )
    1.37 +    body_dummy
    1.38  \<close> ML \<open>
    1.39  \<close>
    1.40  declare [[ML_print_depth = 999]] (* ..for getting complete <Output> *)