From cb4139dc35527bd8c8f9b70753c3d1f552c5f19d Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Wed, 29 Jun 2022 01:14:51 +0200
Subject: 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.
---
 mltt/core/elaborated_statement.ML | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'mltt/core/elaborated_statement.ML')

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;
 
-- 
cgit v1.2.3