changeset 60337 | cbad4e18e91b |
parent 60309 | 70a1d102660d |
child 60436 | 1c8263e775d4 |
1.1 --- a/src/Tools/isac/ProgLang/Program.thy Mon Jul 19 17:29:35 2021 +0200 1.2 +++ b/src/Tools/isac/ProgLang/Program.thy Mon Jul 19 18:29:46 2021 +0200 1.3 @@ -67,8 +67,7 @@ 1.4 |> Thm.prop_of 1.5 |> HOLogic.dest_Trueprop 1.6 |> Logic.unvarify_global 1.7 - |> TermC.inst_abs 1.8 - |> ThmC_Def.num_to_Free (*for numbers in the program*)) 1.9 + |> TermC.inst_abs) 1.10 handle TERM _ => raise TERM ("prep_program", [Thm.prop_of thm]) 1.11 1.12 (* get identifier of partial_function *)