Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Some cleanup
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Nicolas Méric 2023-04-20 07:11:16 +02:00
parent 1acf863845
commit c6dc848438
1 changed files with 5 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -2578,6 +2578,9 @@ ML\<open>
local local
fun elaborate stmt ctxt = stmt |> map (apsnd (map (apfst (DOF_core.elaborate_term ctxt)
#> apsnd (map (DOF_core.elaborate_term ctxt)))))
fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt = fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
let let
val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt; val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt;
@ -2587,11 +2590,7 @@ fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
(case raw_stmt of (case raw_stmt of
Element.Shows _ => Element.Shows _ =>
let val stmt' = Attrib.map_specs (map prep_att) stmt let val stmt' = Attrib.map_specs (map prep_att) stmt
val stmt'' = stmt' |> map (fn (b, ts) => val stmt'' = elaborate stmt' ctxt
(b, ts |> map (fn (t', t's) =>
(DOF_core.elaborate_term ctxt t',
t's |> map (fn t'' =>
DOF_core.elaborate_term ctxt t'')))))
in (([], prems, stmt'', NONE), stmt_ctxt) end in (([], prems, stmt'', NONE), stmt_ctxt) end
| Element.Obtains raw_obtains => | Element.Obtains raw_obtains =>
let let
@ -2606,11 +2605,7 @@ fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
||> Proof_Context.restore_stmt asms_ctxt; ||> Proof_Context.restore_stmt asms_ctxt;
val stmt' = [(Binding.empty_atts, [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])]; val stmt' = [(Binding.empty_atts, [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])];
val stmt'' = stmt' |> map (fn (b, ts) => val stmt'' = elaborate stmt' ctxt
(b, ts |> map (fn (t', t's) =>
(DOF_core.elaborate_term ctxt t',
t's |> map (fn t'' =>
DOF_core.elaborate_term ctxt t'')))))
in ((Obtain.obtains_attribs raw_obtains, prems, stmt'', SOME that'), that_ctxt) end) in ((Obtain.obtains_attribs raw_obtains, prems, stmt'', SOME that'), that_ctxt) end)
end; end;