equal
deleted
inserted
replaced
362 val inst''' = insts'' |> List.last |> snd |> snd; |
362 val inst''' = insts'' |> List.last |> snd |> snd; |
363 val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt; |
363 val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt; |
364 val ctxt'' = Locale.activate_declarations (loc, morph) ctxt; |
364 val ctxt'' = Locale.activate_declarations (loc, morph) ctxt; |
365 in (i + 1, insts', ctxt'') end; |
365 in (i + 1, insts', ctxt'') end; |
366 |
366 |
367 fun prep_elem insts raw_elem ctxt = |
367 fun prep_elem raw_elem ctxt = |
368 let |
368 let |
369 val ctxt' = ctxt |
369 val ctxt' = ctxt |
370 |> Context_Position.set_visible false |
370 |> Context_Position.set_visible false |
371 |> declare_elem prep_vars_elem raw_elem |
371 |> declare_elem prep_vars_elem raw_elem |
372 |> Context_Position.restore_visible ctxt; |
372 |> Context_Position.restore_visible ctxt; |
389 [] => () |
389 [] => () |
390 | frees => error ("Illegal free variables in expression: " ^ |
390 | frees => error ("Illegal free variables in expression: " ^ |
391 commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees)))); |
391 commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees)))); |
392 |
392 |
393 val ctxt4 = init_body ctxt3; |
393 val ctxt4 = init_body ctxt3; |
394 val (elems, ctxt5) = fold_map (prep_elem insts') raw_elems ctxt4; |
394 val (elems, ctxt5) = fold_map prep_elem raw_elems ctxt4; |
395 val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5); |
395 val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5); |
396 |
396 |
397 (* Retrieve parameter types *) |
397 (* Retrieve parameter types *) |
398 val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.check_name o #1) fixes) |
398 val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.check_name o #1) fixes) |
399 | _ => fn ps => ps) (Fixes fors :: elems') []; |
399 | _ => fn ps => ps) (Fixes fors :: elems') []; |