diff options
Diffstat (limited to 'hott/Identity.thy')
| -rw-r--r-- | hott/Identity.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/hott/Identity.thy b/hott/Identity.thy index b9ebafb..b06604f 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -54,7 +54,7 @@ section \<open>Path induction\<close> method_setup eq = \<open>Args.term >> (fn tm => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS ( + CHEADGOAL o SIDE_CONDS 0 ( CONTEXT_SUBGOAL (fn (goal, i) => fn cst as (ctxt, st) => let val facts = Proof_Context.facts_of ctxt |