equal
deleted
inserted
replaced
841 val clauses = map (mk_clause_context x ctxt') abstract_qglrs |
841 val clauses = map (mk_clause_context x ctxt') abstract_qglrs |
842 |
842 |
843 val n = length abstract_qglrs |
843 val n = length abstract_qglrs |
844 |
844 |
845 fun build_tree (ClauseContext { ctxt, rhs, ...}) = |
845 fun build_tree (ClauseContext { ctxt, rhs, ...}) = |
846 Function_Context_Tree.mk_tree fvar h ctxt rhs |
846 Function_Context_Tree.mk_tree (Free fvar) h ctxt rhs |
847 |
847 |
848 val trees = map build_tree clauses |
848 val trees = map build_tree clauses |
849 val RCss = map find_calls trees |
849 val RCss = map find_calls trees |
850 |
850 |
851 val ((G, GIntro_thms, G_elim, G_induct), lthy) = |
851 val ((G, GIntro_thms, G_elim, G_induct), lthy) = |