src/Pure/Tools/find_theorems.ML
changeset 52854 92932931bd82
parent 52851 e71b5160f242
child 52855 fb1f026c48ff
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Aug 02 22:13:31 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 02 22:17:53 2013 +0200
     1.3 @@ -640,12 +640,15 @@
     1.4  
     1.5  (** print function **)
     1.6  
     1.7 -val _ = Command.print_function "find_theorems"
     1.8 +val find_theoremsN = "find_theorems";
     1.9 +
    1.10 +val _ = Command.print_function find_theoremsN
    1.11    (fn {args, ...} =>
    1.12 -    if null args then NONE
    1.13 -    else
    1.14 +    (case args of
    1.15 +      [instance, query] =>
    1.16        SOME {delay = NONE, pri = 0, persistent = false,
    1.17          print_fn = fn _ => fn st =>
    1.18 -          writeln (cat_lines ("find_theorems" :: args))});
    1.19 +          Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)] query}
    1.20 +    | _ => NONE));
    1.21  
    1.22  end;