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/Predicate_Compile/predicate_compile_fun.ML
changeset 55379 9701dbc35f86
parent 54247 81ee85f56e2d
child 55437 3fd63b92ea3b 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Feb 10 13:47:31 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Feb 10 14:33:47 2014 +0100
@@ -285,7 +285,7 @@
         |> Sign.add_consts_i
           (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
            dst_preds)
-        |> fold_map Specification.axiom
+        |> fold_map Specification.axiom  (* FIXME !?!?!?! *)
             (map_index (fn (j, (predname, t)) =>
                 ((Binding.name (Long_Name.base_name predname ^ "_intro_" ^ string_of_int (j + 1)), []), t))
               (maps (uncurry (map o pair)) (prednames ~~ intr_tss)))
isabelle