theory A
imports Main
keywords "define_terms" :: thy_decl
begin

subsection "Main ML implementation"

ML {*
  fun define_terms args lthy =
    let
      val ts = Syntax.read_terms lthy (map snd args);  (* simultaneous read *)
      val specs =
        map2 (fn (b, _) => fn t => ((b, NoSyn), ((Thm.def_binding b, []), t)))
          args ts;
      val (results, lthy') = fold_map Local_Theory.define specs lthy;
      val _ = writeln (PolyML.makestring results);  (* FIXME not for production version *)
    in lthy' end
  
*}

subsection "Outer syntax wrapper"

ML {*
  Outer_Syntax.local_theory @{command_spec "define_terms"} "define some terms"
    (Parse.and_list1 (Parse.binding -- (@{keyword "="} |-- Parse.term)) >> define_terms)
*}


subsection "Example"

define_terms foo = "True" and bar = "\<lambda>x. x"
term foo thm foo_def
term bar thm bar_def

end