Skip to content

Commit

Permalink
Change TFL's notion of sys_var to be (not o Lexis.is_clean_varname)
Browse files Browse the repository at this point in the history
This then stops Unicode variable names from being sys_vars and seems
to resolve TFL bug of a59fe13.
  • Loading branch information
mn200 committed Aug 23, 2019
1 parent 4b1a288 commit 8be7702
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/tfl/src/RW.sml
Original file line number Diff line number Diff line change
Expand Up @@ -276,8 +276,8 @@ fun stringulate _ [] = []

val drop_opt = List.mapPartial Lib.I

local fun sys_var tm = (is_var tm andalso
not(Lexis.ok_identifier(fst(dest_var tm))))
local fun sys_var tm =
is_var tm andalso not (Lexis.is_clean_varname (fst (dest_var tm)))
val failed = RW_ERR "RW_STEP" "all applications failed"
in
fun RW_STEP {context=(cntxt,_),prover,simpls as RW{rw_net,...}} tm = let
Expand Down

0 comments on commit 8be7702

Please sign in to comment.