From a069d566f8146336bea6ed5a1a3b71f339b3c2d6 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Mon, 25 Jun 2018 19:00:09 +0100 Subject: [PATCH] Bug fix: wrong order of default variables. --- Hiding_Type_Variables.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Hiding_Type_Variables.thy b/Hiding_Type_Variables.thy index 92df9f6..2a0cdd0 100644 --- a/Hiding_Type_Variables.thy +++ b/Hiding_Type_Variables.thy @@ -399,7 +399,7 @@ structure Hide_Tvar : HIDE_TVAR = struct | _ => error("Unsupported type structure.") val type_vars_ast = map (fn n => Ast.Variable(name_of_tvar n)) (#tvars default_info) val type_vars_ast = case hole of - right => List.drop(List.rev type_vars_ast, List.length args)@args + right => (List.rev(List.drop(List.rev type_vars_ast, List.length args)))@args | left => args@List.drop(type_vars_ast, List.length args) in Ast.Appl ((Ast.Constant decorated_name)::type_vars_ast)