src/Tools/isac/ProgLang/Prog_Tac.thy
changeset 59861 65ec9f679c3f
parent 59848 06a5cfe04223
child 59868 d77aa0992e0f
     1.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy	Thu Apr 09 12:03:14 2020 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy	Thu Apr 09 17:13:17 2020 +0200
     1.3 @@ -119,8 +119,8 @@
     1.4        | get_t (Const ("Prog_Tac.SubProblem",_) $ _ $ _) _ = NONE
     1.5  
     1.6        | get_t _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
     1.7 -    in get_t body Rule.e_term end
     1.8 -  | get_first_argument t = error ("get_first_argument: no fun-def. for " ^ Rule.term2str t);
     1.9 +    in get_t body TermC.empty end
    1.10 +  | get_first_argument t = error ("get_first_argument: no fun-def. for " ^ UnparseC.term2str t);
    1.11  
    1.12  (* substitute the Istate.T's environment to a leaf of the program
    1.13     and attach the curried argument of a tactic, if any.