equal
deleted
inserted
replaced
29 Theory.setup |
29 Theory.setup |
30 (setup_trace_method @{binding print_fact} |
30 (setup_trace_method @{binding print_fact} |
31 (Scan.lift (Scan.ahead Parse.not_eof) -- Attrib.thms) |
31 (Scan.lift (Scan.ahead Parse.not_eof) -- Attrib.thms) |
32 (fn ctxt => fn (tok, thms) => |
32 (fn ctxt => fn (tok, thms) => |
33 (* FIXME proper formatting!? *) |
33 (* FIXME proper formatting!? *) |
34 Token.unparse tok ^ ": " ^ commas (map (Display.string_of_thm ctxt) thms)) #> |
34 Token.unparse tok ^ ": " ^ commas (map (Thm.string_of_thm ctxt) thms)) #> |
35 setup_trace_method @{binding print_term} |
35 setup_trace_method @{binding print_term} |
36 (Scan.lift (Scan.ahead Parse.not_eof) -- Args.term) |
36 (Scan.lift (Scan.ahead Parse.not_eof) -- Args.term) |
37 (fn ctxt => fn (tok, t) => |
37 (fn ctxt => fn (tok, t) => |
38 (* FIXME proper formatting!? *) |
38 (* FIXME proper formatting!? *) |
39 Token.unparse tok ^ ": " ^ Syntax.string_of_term ctxt t) #> |
39 Token.unparse tok ^ ": " ^ Syntax.string_of_term ctxt t) #> |