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.
Fixed bug in fact activation.
authorballarin
Tue, 26 Apr 2005 09:24:58 +0200
changeset 15839 12b06f56209a
parent 15838 2aee4e5b7925
child 15840 462ea9188823
Fixed bug in fact activation.
src/Pure/Isar/locale.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/locale.ML	Mon Apr 25 18:29:40 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Apr 26 09:24:58 2005 +0200
@@ -2052,7 +2052,7 @@
                 handle Option => error ("(internal) unknown registration of " ^
                   quote (fst id) ^ " while activating facts.")) all_elemss);
       in Library.foldl (activate_facts_elems get_reg note_thmss attrib
-        (Drule.standard o Drule.fconv_rule (Thm.beta_conversion true) o
+        (standard o Drule.fconv_rule (Thm.beta_conversion true) o
           Drule.satisfy_hyps prems)) (thy_ctxt, new_elemss) end;
 
 val global_activate_facts_elemss = gen_activate_facts_elemss
isabelle