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/SPARK/Tools/spark_vcs.ML
changeset 61259 6dc3d5d50e57
parent 61246 077b88f9ec16
child 61260 e6f03fae14d5 
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Sep 23 09:36:18 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Sep 23 09:50:38 2015 +0200
@@ -388,8 +388,7 @@
       (ids,
        case get_type thy prfx s of
          SOME _ => thy
-       | NONE => Typedecl.typedecl_global
-           true (Binding.name s, [], NoSyn) thy |> snd);
+       | NONE => Typedecl.typedecl_global {final = true} (Binding.name s, [], NoSyn) thy |> snd);
 
 
 fun term_of_expr thy prfx types pfuns =
isabelle