equal
deleted
inserted
replaced
380 in normh end; |
380 in normh end; |
381 |
381 |
382 |
382 |
383 (* dummy patterns *) |
383 (* dummy patterns *) |
384 |
384 |
385 fun is_dummy (Const ("dummy", _)) = true |
385 fun is_dummy (Const (c, _)) = c = PureThy.dummy_patternN |
386 | is_dummy _ = false; |
386 | is_dummy _ = false; |
387 |
387 |
388 fun reject_dummies ctxt tm = |
388 fun reject_dummies ctxt tm = |
389 if foldl_aterms (fn (ok, t) => ok andalso not (is_dummy t)) (true, tm) then tm |
389 if foldl_aterms (fn (ok, t) => ok andalso not (is_dummy t)) (true, tm) then tm |
390 else raise CONTEXT ("Illegal dummy pattern(s) in term", ctxt); |
390 else raise CONTEXT ("Illegal dummy pattern(s) in term", ctxt); |
391 |
391 |
392 |
392 |
393 fun prep_dummy (i, Const ("dummy", T)) = (i + 1, Var (("_dummy_", i), T)) |
393 fun prep_dummy (i, t) = |
394 | prep_dummy i_t = i_t; |
394 if is_dummy t then (i + 1, Var (("_dummy_", i), Term.fastype_of t)) else (i, t); |
395 |
395 |
396 fun prepare_dummies tm = #2 (Term.foldl_map_aterms prep_dummy (1, tm)); |
396 fun prepare_dummies tm = #2 (Term.foldl_map_aterms prep_dummy (1, tm)); |
397 |
397 |
398 |
398 |
399 (* read terms *) |
399 (* read terms *) |