src/Tools/isac/ProgLang/Program.thy
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 *)