# HG changeset patch # User wenzelm # Date 1434378292 -7200 # Node ID fa31b5d36bebaa7612b48eb79050993dea916e56 # Parent 17a2dae7d2462a4a734dde3e8be33904226094cd tuned signature; diff -r 17a2dae7d246 -r fa31b5d36beb src/HOL/Tools/functor.ML --- a/src/HOL/Tools/functor.ML Mon Jun 15 15:34:29 2015 +0200 +++ b/src/HOL/Tools/functor.ML Mon Jun 15 16:24:52 2015 +0200 @@ -9,7 +9,7 @@ val find_atomic: Proof.context -> typ -> (typ * (bool * bool)) list val construct_mapper: Proof.context -> (string * bool -> term) -> bool -> typ -> typ -> term - val functorx: string option -> term -> local_theory -> Proof.state + val functor_: string option -> term -> local_theory -> Proof.state val functor_cmd: string option -> string -> Proof.context -> Proof.state type entry val entries: Proof.context -> entry list Symtab.table @@ -269,7 +269,7 @@ |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop]) end -val functorx = gen_functor Syntax.check_term; +val functor_ = gen_functor Syntax.check_term; val functor_cmd = gen_functor Syntax.read_term; val _ =