Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/functor.ML
changeset 60488 fa31b5d36beb
parent 59936 b8ffc3dc9e24
child 61841 4d3527b94f2a 
--- 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