adbrucker
/
isabelle-hacks
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Cleanup of parse translation hide_tvar_subst_ast_tr.

This commit is contained in:
Achim D. Brucker 2018-06-22 15:45:29 +01:00
parent 3c1b07e065
commit 251414e8b4
1 changed files with 0 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Hiding_Type_Variables.thy
View File

@ -363,9 +363,6 @@ datatype tvar_subst = right | left
fun hide_tvar_subst_ast_tr hole ctx (ast::[]) =
let
val thy = Proof_Context.theory_of ctx
fun string_of_ast (Ast.Constant s) = "(C"^s^")"
| string_of_ast (Ast.Variable s) = "(V"^s^")"
| string_of_ast (Ast.Appl ast) = String.concat (map string_of_ast ast)
val (decorated_name, args) = case ast
of (Ast.Appl ((Ast.Constant s)::args)) => (s, args)
| _ => error "Error in obtaining type constructor."