changeset 61246 | 077b88f9ec16 |
parent 60754 | 02924903a6fd |
child 61259 | 6dc3d5d50e57 |
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Tue Sep 22 08:38:25 2015 +0200 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Tue Sep 22 14:32:23 2015 +0200 @@ -389,7 +389,7 @@ case get_type thy prfx s of SOME _ => thy | NONE => Typedecl.typedecl_global - (Binding.name s, [], NoSyn) thy |> snd); + true (Binding.name s, [], NoSyn) thy |> snd); fun term_of_expr thy prfx types pfuns =