From ac0fa734e46c2b265d2c58a3e88501fd5497b31b Mon Sep 17 00:00:00 2001 From: Michael Herzberg Date: Thu, 25 Jul 2019 16:27:10 +0100 Subject: [PATCH] Added support for multiple sorts in shortened type variables. --- Core_DOM/preliminaries/Hiding_Type_Variables.thy | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/Core_DOM/preliminaries/Hiding_Type_Variables.thy b/Core_DOM/preliminaries/Hiding_Type_Variables.thy index 3c593ef..e31e560 100644 --- a/Core_DOM/preliminaries/Hiding_Type_Variables.thy +++ b/Core_DOM/preliminaries/Hiding_Type_Variables.thy @@ -276,9 +276,8 @@ structure Hide_Tvar : HIDE_TVAR = struct val thy = Proof_Context.theory_of ctx fun parse_ast ((Ast.Constant const)::[]) = (const,NONE) - | parse_ast ((Ast.Constant sort)::(Ast.Constant const)::[]) - = (const,SOME sort) - | parse_ast _ = error("AST type not supported.") + | parse_ast (sort::(Ast.Constant const)::[]) = (const,SOME sort) + | parse_ast _ = error("AST type not supported.") val (decorated_name, decorated_sort) = parse_ast ast @@ -295,9 +294,9 @@ structure Hide_Tvar : HIDE_TVAR = struct let fun mk_tvar n = case decorated_sort of NONE => Ast.Variable(name_of_tvar n) - | SOME sort => Ast.Appl([Ast.Constant("_ofsort"), + | SOME sort => Ast.Appl([Ast.Constant("_ofsort"), Ast.Variable(name_of_tvar n), - Ast.Constant(sort)]) + sort]) in map mk_tvar (#tvars default_info) end