Mercurial Mercurial > hg > nominal2 / 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.
Nominal/nominal_function_core.ML
changeset 2885 1264f2a21ea9
parent 2862 47063163f333
child 2973 d1038e67923a 
--- a/Nominal/nominal_function_core.ML	Wed Jun 22 17:57:15 2011 +0900
+++ b/Nominal/nominal_function_core.ML	Wed Jun 22 12:18:22 2011 +0100
@@ -589,7 +589,7 @@
   let
     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
       lthy
-      |> Local_Theory.conceal 
+      |> Local_Theory.conceal
       |> Inductive.add_inductive_i
           {quiet_mode = true,
             verbose = ! trace,
nominal2