equal
deleted
inserted
replaced
55 #> Scan.read Token.stopper Method.parse |
55 #> Scan.read Token.stopper Method.parse |
56 #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source"); |
56 #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source"); |
57 |
57 |
58 fun apply_named_method_on_first_goal ctxt = |
58 fun apply_named_method_on_first_goal ctxt = |
59 parse_method |
59 parse_method |
60 #> Method.check_source ctxt |
60 #> Method.method_cmd ctxt |
61 #> Method.the_method ctxt |
|
62 #> Method.Basic |
61 #> Method.Basic |
63 #> (fn m => Method.Select_Goals (Method.no_combinator_info, 1, m)) |
62 #> (fn m => Method.Select_Goals (Method.no_combinator_info, 1, m)) |
64 #> Proof.refine; |
63 #> Proof.refine; |
65 |
64 |
66 fun add_attr_text (NONE, _) s = s |
65 fun add_attr_text (NONE, _) s = s |