diff options
author | stuebinm | 2022-06-29 01:14:51 +0200 |
---|---|---|
committer | stuebinm | 2022-06-29 01:23:31 +0200 |
commit | cb4139dc35527bd8c8f9b70753c3d1f552c5f19d (patch) | |
tree | 8e5709039197ad6d72d8b38235a982bf687e2608 /mltt/core/elaborated_statement.ML | |
parent | 5655750e12d3459c1237588f8dec3fc883a966b7 (diff) |
make mltt work with isabelle 2021-1
notably, this modifies the proof method `this`: the previous version
of it no longer works with cconv.ML (borrowed from HOL), so now it's
just a call to the simplifier, which does work.
Unfortunately the new `this` can otherwise do less than the old one
(it does not instantiate schematic variables), so the old one is now
available as `infer` instead.
Diffstat (limited to 'mltt/core/elaborated_statement.ML')
-rw-r--r-- | mltt/core/elaborated_statement.ML | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/mltt/core/elaborated_statement.ML b/mltt/core/elaborated_statement.ML index 33f88cf..2e129c8 100644 --- a/mltt/core/elaborated_statement.ML +++ b/mltt/core/elaborated_statement.ML @@ -95,12 +95,14 @@ fun inst_morphism params ((prfx, mandatory), insts') ctxt = (*instantiation*) val instT = (type_parms ~~ map Logic.dest_type type_parms'') - |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T)); + |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T)) + |> TFrees.make; val cert_inst = ((map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'') - |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t)); + |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t)) + |> Frees.make; in - (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $> + (Element.instantiate_normalize_morphism (TFrees.map (K certT) instT, cert_inst) $> Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt') end; |