Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Mon, 15 Jun 2015 16:24:52 +0200
changeset 60488 fa31b5d36beb
parent 60486 17a2dae7d246
child 60489 bfd9b7302a82
tuned signature;
src/HOL/Tools/functor.ML file | annotate | diff | comparison | revisions 
--- 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 _ =
isabelle