adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Isabelle2017: update AutoCorres for RC0 

* Named_Target.init removed redundant parameter.
This commit is contained in:
Matthew Brecknell 2017-08-29 09:38:34 +10:00
parent 3cb118fe02
commit 8f2f5df099
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tools/autocorres/heap_lift_base.ML
View File

@ -436,7 +436,7 @@ let
* HACK: Exit and enter the context again, so the simpset created by the new
* record gets imported in. No idea what the "correct" way of doing this is.
*)
val lthy = Local_Theory.exit_global lthy |> Named_Target.init NONE (the (Named_Target.locale_of lthy))
val lthy = Local_Theory.exit_global lthy |> Named_Target.init (the (Named_Target.locale_of lthy))
(* Generate a function mapping old globals to the new globals. *)
val (lift_name, lift_def, simp_thms, lthy) = gen_heap_abs_fn